(0) Obligation:

Clauses:

e(a, b).
q(X, Y) :- e(X, Y).
q(X, f(f(X))) :- ','(p(X, f(f(X))), q(X, f(X))).
q(X, f(f(Y))) :- p(X, f(Y)).
p(X, Y) :- e(X, Y).
p(X, f(Y)) :- ','(r(X, f(Y)), p(X, Y)).
r(X, Y) :- e(X, Y).
r(X, f(Y)) :- ','(q(X, Y), r(X, Y)).
r(f(X), f(X)) :- t(f(X), f(X)).
t(X, Y) :- e(X, Y).
t(f(X), f(Y)) :- ','(q(f(X), f(Y)), t(X, Y)).

Query: q(g,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

qA(f(X1)) :- pB(f(X1)).
pF(X1, X2) :- qC(f(X1), X2).
pF(X1, f(X2)) :- ','(qcC(f(X1), f(X2)), pF(X1, X2)).
pF(X1, f(X1)) :- ','(qcC(f(X1), f(X1)), tG(X1)).
qH(f(f(X1))) :- pI(X1).
pJ(X1) :- qH(f(X1)).
pJ(f(X1)) :- ','(qcH(f(f(X1))), pJ(X1)).
tG(X1) :- pJ(X1).
pK(X1, X2) :- pF(X1, X2).
pK(X1, X1) :- tG(X1).
pK(X1, f(X2)) :- ','(rcL(X1, f(X2)), pK(X1, X2)).
pM(X1, X2) :- pK(X1, X2).
rN(f(f(f(X1)))) :- pM(f(f(f(f(f(f(f(f(X1)))))))), X1).
rN(f(f(X1))) :- ','(qcO(f(X1)), pF(f(f(f(f(f(f(f(X1))))))), X1)).
pP(f(X1)) :- rN(f(X1)).
pP(f(f(X1))) :- ','(rcN(f(f(X1))), pK(f(f(f(f(f(f(f(X1))))))), X1)).
pQ(f(f(X1))) :- pM(f(f(f(f(f(f(f(X1))))))), X1).
pQ(X1) :- ','(qcR(X1), rN(X1)).
rS(f(f(f(X1)))) :- pP(f(X1)).
rS(f(f(X1))) :- ','(qcT(f(X1)), pQ(X1)).
pU(X1) :- pQ(X1).
pU(X1) :- ','(rcV(X1), pP(X1)).
pW(f(X1)) :- rS(f(X1)).
pW(f(f(X1))) :- ','(rcS(f(f(X1))), pU(X1)).
pX(f(f(X1))) :- pU(X1).
pX(X1) :- ','(qcY(X1), rS(X1)).
rZ(f(f(f(X1)))) :- pW(f(X1)).
rZ(f(f(X1))) :- ','(qcN1(f(X1)), pX(X1)).
pN2(X1) :- pX(X1).
pN2(X1) :- ','(rcN3(X1), pW(X1)).
pN4(f(X1)) :- rZ(f(X1)).
pN4(f(f(X1))) :- ','(rcZ(f(f(X1))), pN2(X1)).
pN5(f(f(X1))) :- pN2(X1).
pN5(X1) :- ','(qcN6(X1), rZ(X1)).
rN7(X1) :- qH(X1).
rN7(X1) :- ','(qcH(X1), rN8(X1)).
rN8(f(f(f(X1)))) :- pN4(f(X1)).
rN8(f(f(X1))) :- ','(qcN9(f(X1)), pN5(X1)).
rN8(f(X1)) :- tG(X1).
pI(X1) :- pN5(X1).
pI(X1) :- ','(rcN10(X1), pN4(X1)).
pB(f(X1)) :- rN8(f(X1)).
pB(f(f(X1))) :- ','(rcN8(f(f(X1))), pI(X1)).
pN11(X1, X2) :- qC(X1, X2).
pN11(X1, f(X2)) :- ','(qcC(X1, f(X2)), pN11(X1, X2)).
pN11(f(X1), f(X1)) :- ','(qcC(f(X1), f(X1)), tG(X1)).
pE(X1, X2) :- pN11(X1, X2).
pE(f(X1), X1) :- tG(X1).
pE(X1, f(X2)) :- ','(rcN12(X1, f(X2)), pE(X1, X2)).
qC(X1, f(f(X1))) :- qA(X1).
qC(X1, f(f(X1))) :- ','(qcA(X1), rN7(X1)).
qC(X1, f(f(X1))) :- ','(rcN13(X1), rN7(X1)).
qC(X1, f(f(X1))) :- ','(rcN13(X1), ','(rcN7(X1), pB(X1))).
qC(X1, f(f(X1))) :- ','(pcD(X1), qA(X1)).
qC(X1, f(f(X2))) :- pE(X1, X2).

Clauses:

qcA(f(X1)) :- pcB(f(X1)).
qcC(a, b).
qcC(X1, f(f(X1))) :- ','(pcD(X1), qcA(X1)).
qcC(X1, f(f(X2))) :- qcE(X1, X2).
qcF(X1, f(X2)) :- ','(qcC(f(X1), f(X2)), qcF(X1, X2)).
qcF(X1, f(X1)) :- ','(qcC(f(X1), f(X1)), tcG(X1)).
qcH(f(f(X1))) :- qcI(X1).
qcJ(f(X1)) :- ','(qcH(f(f(X1))), qcJ(X1)).
tcG(X1) :- qcJ(X1).
qcK(X1, f(X2)) :- ','(rcL(X1, f(X2)), qcK(X1, X2)).
pcM(X1, X2) :- qcK(X1, X2).
rcN(f(f(X1))) :- ','(qcO(f(X1)), qcF(f(f(f(f(f(f(f(X1))))))), X1)).
pcP(f(f(X1))) :- ','(rcN(f(f(X1))), qcK(f(f(f(f(f(f(f(X1))))))), X1)).
qcQ(X1) :- ','(qcR(X1), rcN(X1)).
rcS(f(f(X1))) :- ','(qcT(f(X1)), qcQ(X1)).
qcU(X1) :- ','(rcV(X1), pcP(X1)).
pcW(f(f(X1))) :- ','(rcS(f(f(X1))), qcU(X1)).
qcX(X1) :- ','(qcY(X1), rcS(X1)).
rcZ(f(f(X1))) :- ','(qcN1(f(X1)), qcX(X1)).
qcN2(X1) :- ','(rcN3(X1), pcW(X1)).
pcN4(f(f(X1))) :- ','(rcZ(f(f(X1))), qcN2(X1)).
qcN5(X1) :- ','(qcN6(X1), rcZ(X1)).
rcN7(X1) :- ','(qcH(X1), rcN8(X1)).
rcN8(f(f(X1))) :- ','(qcN9(f(X1)), qcN5(X1)).
rcN8(f(X1)) :- tcG(X1).
qcI(X1) :- ','(rcN10(X1), pcN4(X1)).
pcB(f(f(X1))) :- ','(rcN8(f(f(X1))), qcI(X1)).
qcN11(a, b) :- qcC(a, b).
qcN11(X1, f(X2)) :- ','(qcC(X1, f(X2)), qcN11(X1, X2)).
qcN11(f(X1), f(X1)) :- ','(qcC(f(X1), f(X1)), tcG(X1)).
qcE(a, b) :- rcN12(a, b).
qcE(X1, f(X2)) :- ','(rcN12(X1, f(X2)), qcE(X1, X2)).
pcD(X1) :- ','(rcN13(X1), ','(rcN7(X1), pcB(X1))).
rcN13(X1) :- ','(qcA(X1), rcN7(X1)).
rcN10(X1) :- qcN5(X1).
qcN6(f(f(X1))) :- qcN2(X1).
rcN3(X1) :- qcX(X1).
qcY(f(f(X1))) :- qcU(X1).
rcV(X1) :- qcQ(X1).
qcR(f(f(X1))) :- pcM(f(f(f(f(f(f(f(X1))))))), X1).
rcL(X1, X2) :- qcF(X1, X2).
rcL(X1, X1) :- tcG(X1).
qcO(f(f(X1))) :- pcM(f(f(f(f(f(f(f(f(X1)))))))), X1).
qcT(f(f(X1))) :- pcP(f(X1)).
qcN1(f(f(X1))) :- pcW(f(X1)).
qcN9(f(f(X1))) :- pcN4(f(X1)).
rcN12(X1, X2) :- qcN11(X1, X2).
rcN12(f(X1), X1) :- tcG(X1).

Afs:

qC(x1, x2)  =  qC(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
qC_in: (b,b)
qA_in: (b)
pB_in: (b)
rN8_in: (b)
pN4_in: (b)
rZ_in: (b)
pW_in: (b)
rS_in: (b)
pP_in: (b)
rN_in: (b)
pM_in: (b,b)
pK_in: (b,b)
pF_in: (b,b)
qcA_in: (b)
pcB_in: (b)
rcN8_in: (b)
qcN9_in: (b)
pcN4_in: (b)
rcZ_in: (b)
qcN1_in: (b)
pcW_in: (b)
rcS_in: (b)
qcT_in: (b)
pcP_in: (b)
rcN_in: (b)
qcO_in: (b)
pcM_in: (b,b)
qcK_in: (b,b)
rcL_in: (b,b)
qcF_in: (b,b)
qcC_in: (b,b)
pcD_in: (b)
rcN13_in: (b)
rcN7_in: (b)
qcH_in: (b)
qcI_in: (b)
rcN10_in: (b)
qcN5_in: (b)
qcN6_in: (b)
qcN2_in: (b)
rcN3_in: (b)
qcX_in: (b)
qcY_in: (b)
qcU_in: (b)
rcV_in: (b)
qcQ_in: (b)
qcR_in: (b)
tcG_in: (b)
qcJ_in: (b)
qcE_in: (b,b)
rcN12_in: (b,b)
qcN11_in: (b,b)
rN7_in: (b)
qH_in: (b)
pI_in: (b)
pN5_in: (b)
pN2_in: (b)
pX_in: (b)
pU_in: (b)
pQ_in: (b)
tG_in: (b)
pJ_in: (b)
pE_in: (b,b)
pN11_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

QC_IN_GG(X1, f(f(X1))) → U72_GG(X1, qA_in_g(X1))
QC_IN_GG(X1, f(f(X1))) → QA_IN_G(X1)
QA_IN_G(f(X1)) → U1_G(X1, pB_in_g(f(X1)))
QA_IN_G(f(X1)) → PB_IN_G(f(X1))
PB_IN_G(f(X1)) → U60_G(X1, rN8_in_g(f(X1)))
PB_IN_G(f(X1)) → RN8_IN_G(f(X1))
RN8_IN_G(f(f(f(X1)))) → U53_G(X1, pN4_in_g(f(X1)))
RN8_IN_G(f(f(f(X1)))) → PN4_IN_G(f(X1))
PN4_IN_G(f(X1)) → U44_G(X1, rZ_in_g(f(X1)))
PN4_IN_G(f(X1)) → RZ_IN_G(f(X1))
RZ_IN_G(f(f(f(X1)))) → U38_G(X1, pW_in_g(f(X1)))
RZ_IN_G(f(f(f(X1)))) → PW_IN_G(f(X1))
PW_IN_G(f(X1)) → U32_G(X1, rS_in_g(f(X1)))
PW_IN_G(f(X1)) → RS_IN_G(f(X1))
RS_IN_G(f(f(f(X1)))) → U26_G(X1, pP_in_g(f(X1)))
RS_IN_G(f(f(f(X1)))) → PP_IN_G(f(X1))
PP_IN_G(f(X1)) → U20_G(X1, rN_in_g(f(X1)))
PP_IN_G(f(X1)) → RN_IN_G(f(X1))
RN_IN_G(f(f(f(X1)))) → U17_G(X1, pM_in_gg(f(f(f(f(f(f(f(f(X1)))))))), X1))
RN_IN_G(f(f(f(X1)))) → PM_IN_GG(f(f(f(f(f(f(f(f(X1)))))))), X1)
PM_IN_GG(X1, X2) → U16_GG(X1, X2, pK_in_gg(X1, X2))
PM_IN_GG(X1, X2) → PK_IN_GG(X1, X2)
PK_IN_GG(X1, X2) → U12_GG(X1, X2, pF_in_gg(X1, X2))
PK_IN_GG(X1, X2) → PF_IN_GG(X1, X2)
PF_IN_GG(X1, X2) → U2_GG(X1, X2, qC_in_gg(f(X1), X2))
PF_IN_GG(X1, X2) → QC_IN_GG(f(X1), X2)
QC_IN_GG(X1, f(f(X1))) → U73_GG(X1, qcA_in_g(X1))
U73_GG(X1, qcA_out_g(X1)) → U74_GG(X1, rN7_in_g(X1))
U73_GG(X1, qcA_out_g(X1)) → RN7_IN_G(X1)
RN7_IN_G(X1) → U50_G(X1, qH_in_g(X1))
RN7_IN_G(X1) → QH_IN_G(X1)
QH_IN_G(f(f(X1))) → U7_G(X1, pI_in_g(X1))
QH_IN_G(f(f(X1))) → PI_IN_G(X1)
PI_IN_G(X1) → U57_G(X1, pN5_in_g(X1))
PI_IN_G(X1) → PN5_IN_G(X1)
PN5_IN_G(f(f(X1))) → U47_G(X1, pN2_in_g(X1))
PN5_IN_G(f(f(X1))) → PN2_IN_G(X1)
PN2_IN_G(X1) → U41_G(X1, pX_in_g(X1))
PN2_IN_G(X1) → PX_IN_G(X1)
PX_IN_G(f(f(X1))) → U35_G(X1, pU_in_g(X1))
PX_IN_G(f(f(X1))) → PU_IN_G(X1)
PU_IN_G(X1) → U29_G(X1, pQ_in_g(X1))
PU_IN_G(X1) → PQ_IN_G(X1)
PQ_IN_G(f(f(X1))) → U23_G(X1, pM_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
PQ_IN_G(f(f(X1))) → PM_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PQ_IN_G(X1) → U24_G(X1, qcR_in_g(X1))
U24_G(X1, qcR_out_g(X1)) → U25_G(X1, rN_in_g(X1))
U24_G(X1, qcR_out_g(X1)) → RN_IN_G(X1)
RN_IN_G(f(f(X1))) → U18_G(X1, qcO_in_g(f(X1)))
U18_G(X1, qcO_out_g(f(X1))) → U19_G(X1, pF_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U18_G(X1, qcO_out_g(f(X1))) → PF_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PF_IN_GG(X1, f(X2)) → U3_GG(X1, X2, qcC_in_gg(f(X1), f(X2)))
U3_GG(X1, X2, qcC_out_gg(f(X1), f(X2))) → U4_GG(X1, X2, pF_in_gg(X1, X2))
U3_GG(X1, X2, qcC_out_gg(f(X1), f(X2))) → PF_IN_GG(X1, X2)
PF_IN_GG(X1, f(X1)) → U5_GG(X1, qcC_in_gg(f(X1), f(X1)))
U5_GG(X1, qcC_out_gg(f(X1), f(X1))) → U6_GG(X1, tG_in_g(X1))
U5_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
TG_IN_G(X1) → U11_G(X1, pJ_in_g(X1))
TG_IN_G(X1) → PJ_IN_G(X1)
PJ_IN_G(X1) → U8_G(X1, qH_in_g(f(X1)))
PJ_IN_G(X1) → QH_IN_G(f(X1))
PJ_IN_G(f(X1)) → U9_G(X1, qcH_in_g(f(f(X1))))
U9_G(X1, qcH_out_g(f(f(X1)))) → U10_G(X1, pJ_in_g(X1))
U9_G(X1, qcH_out_g(f(f(X1)))) → PJ_IN_G(X1)
PU_IN_G(X1) → U30_G(X1, rcV_in_g(X1))
U30_G(X1, rcV_out_g(X1)) → U31_G(X1, pP_in_g(X1))
U30_G(X1, rcV_out_g(X1)) → PP_IN_G(X1)
PP_IN_G(f(f(X1))) → U21_G(X1, rcN_in_g(f(f(X1))))
U21_G(X1, rcN_out_g(f(f(X1)))) → U22_G(X1, pK_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U21_G(X1, rcN_out_g(f(f(X1)))) → PK_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PK_IN_GG(X1, X1) → U13_GG(X1, tG_in_g(X1))
PK_IN_GG(X1, X1) → TG_IN_G(X1)
PK_IN_GG(X1, f(X2)) → U14_GG(X1, X2, rcL_in_gg(X1, f(X2)))
U14_GG(X1, X2, rcL_out_gg(X1, f(X2))) → U15_GG(X1, X2, pK_in_gg(X1, X2))
U14_GG(X1, X2, rcL_out_gg(X1, f(X2))) → PK_IN_GG(X1, X2)
PX_IN_G(X1) → U36_G(X1, qcY_in_g(X1))
U36_G(X1, qcY_out_g(X1)) → U37_G(X1, rS_in_g(X1))
U36_G(X1, qcY_out_g(X1)) → RS_IN_G(X1)
RS_IN_G(f(f(X1))) → U27_G(X1, qcT_in_g(f(X1)))
U27_G(X1, qcT_out_g(f(X1))) → U28_G(X1, pQ_in_g(X1))
U27_G(X1, qcT_out_g(f(X1))) → PQ_IN_G(X1)
PN2_IN_G(X1) → U42_G(X1, rcN3_in_g(X1))
U42_G(X1, rcN3_out_g(X1)) → U43_G(X1, pW_in_g(X1))
U42_G(X1, rcN3_out_g(X1)) → PW_IN_G(X1)
PW_IN_G(f(f(X1))) → U33_G(X1, rcS_in_g(f(f(X1))))
U33_G(X1, rcS_out_g(f(f(X1)))) → U34_G(X1, pU_in_g(X1))
U33_G(X1, rcS_out_g(f(f(X1)))) → PU_IN_G(X1)
PN5_IN_G(X1) → U48_G(X1, qcN6_in_g(X1))
U48_G(X1, qcN6_out_g(X1)) → U49_G(X1, rZ_in_g(X1))
U48_G(X1, qcN6_out_g(X1)) → RZ_IN_G(X1)
RZ_IN_G(f(f(X1))) → U39_G(X1, qcN1_in_g(f(X1)))
U39_G(X1, qcN1_out_g(f(X1))) → U40_G(X1, pX_in_g(X1))
U39_G(X1, qcN1_out_g(f(X1))) → PX_IN_G(X1)
PI_IN_G(X1) → U58_G(X1, rcN10_in_g(X1))
U58_G(X1, rcN10_out_g(X1)) → U59_G(X1, pN4_in_g(X1))
U58_G(X1, rcN10_out_g(X1)) → PN4_IN_G(X1)
PN4_IN_G(f(f(X1))) → U45_G(X1, rcZ_in_g(f(f(X1))))
U45_G(X1, rcZ_out_g(f(f(X1)))) → U46_G(X1, pN2_in_g(X1))
U45_G(X1, rcZ_out_g(f(f(X1)))) → PN2_IN_G(X1)
RN7_IN_G(X1) → U51_G(X1, qcH_in_g(X1))
U51_G(X1, qcH_out_g(X1)) → U52_G(X1, rN8_in_g(X1))
U51_G(X1, qcH_out_g(X1)) → RN8_IN_G(X1)
RN8_IN_G(f(f(X1))) → U54_G(X1, qcN9_in_g(f(X1)))
U54_G(X1, qcN9_out_g(f(X1))) → U55_G(X1, pN5_in_g(X1))
U54_G(X1, qcN9_out_g(f(X1))) → PN5_IN_G(X1)
RN8_IN_G(f(X1)) → U56_G(X1, tG_in_g(X1))
RN8_IN_G(f(X1)) → TG_IN_G(X1)
QC_IN_GG(X1, f(f(X1))) → U75_GG(X1, rcN13_in_g(X1))
U75_GG(X1, rcN13_out_g(X1)) → U76_GG(X1, rN7_in_g(X1))
U75_GG(X1, rcN13_out_g(X1)) → RN7_IN_G(X1)
U75_GG(X1, rcN13_out_g(X1)) → U77_GG(X1, rcN7_in_g(X1))
U77_GG(X1, rcN7_out_g(X1)) → U78_GG(X1, pB_in_g(X1))
U77_GG(X1, rcN7_out_g(X1)) → PB_IN_G(X1)
PB_IN_G(f(f(X1))) → U61_G(X1, rcN8_in_g(f(f(X1))))
U61_G(X1, rcN8_out_g(f(f(X1)))) → U62_G(X1, pI_in_g(X1))
U61_G(X1, rcN8_out_g(f(f(X1)))) → PI_IN_G(X1)
QC_IN_GG(X1, f(f(X1))) → U79_GG(X1, pcD_in_g(X1))
U79_GG(X1, pcD_out_g(X1)) → U80_GG(X1, qA_in_g(X1))
U79_GG(X1, pcD_out_g(X1)) → QA_IN_G(X1)
QC_IN_GG(X1, f(f(X2))) → U81_GG(X1, X2, pE_in_gg(X1, X2))
QC_IN_GG(X1, f(f(X2))) → PE_IN_GG(X1, X2)
PE_IN_GG(X1, X2) → U68_GG(X1, X2, pN11_in_gg(X1, X2))
PE_IN_GG(X1, X2) → PN11_IN_GG(X1, X2)
PN11_IN_GG(X1, X2) → U63_GG(X1, X2, qC_in_gg(X1, X2))
PN11_IN_GG(X1, X2) → QC_IN_GG(X1, X2)
PN11_IN_GG(X1, f(X2)) → U64_GG(X1, X2, qcC_in_gg(X1, f(X2)))
U64_GG(X1, X2, qcC_out_gg(X1, f(X2))) → U65_GG(X1, X2, pN11_in_gg(X1, X2))
U64_GG(X1, X2, qcC_out_gg(X1, f(X2))) → PN11_IN_GG(X1, X2)
PN11_IN_GG(f(X1), f(X1)) → U66_GG(X1, qcC_in_gg(f(X1), f(X1)))
U66_GG(X1, qcC_out_gg(f(X1), f(X1))) → U67_GG(X1, tG_in_g(X1))
U66_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
PE_IN_GG(f(X1), X1) → U69_GG(X1, tG_in_g(X1))
PE_IN_GG(f(X1), X1) → TG_IN_G(X1)
PE_IN_GG(X1, f(X2)) → U70_GG(X1, X2, rcN12_in_gg(X1, f(X2)))
U70_GG(X1, X2, rcN12_out_gg(X1, f(X2))) → U71_GG(X1, X2, pE_in_gg(X1, X2))
U70_GG(X1, X2, rcN12_out_gg(X1, f(X2))) → PE_IN_GG(X1, X2)

The TRS R consists of the following rules:

qcA_in_g(f(X1)) → U83_g(X1, pcB_in_g(f(X1)))
pcB_in_g(f(f(X1))) → U127_g(X1, rcN8_in_g(f(f(X1))))
rcN8_in_g(f(f(X1))) → U122_g(X1, qcN9_in_g(f(X1)))
qcN9_in_g(f(f(X1))) → U153_g(X1, pcN4_in_g(f(X1)))
pcN4_in_g(f(f(X1))) → U116_g(X1, rcZ_in_g(f(f(X1))))
rcZ_in_g(f(f(X1))) → U112_g(X1, qcN1_in_g(f(X1)))
qcN1_in_g(f(f(X1))) → U152_g(X1, pcW_in_g(f(X1)))
pcW_in_g(f(f(X1))) → U108_g(X1, rcS_in_g(f(f(X1))))
rcS_in_g(f(f(X1))) → U104_g(X1, qcT_in_g(f(X1)))
qcT_in_g(f(f(X1))) → U151_g(X1, pcP_in_g(f(X1)))
pcP_in_g(f(f(X1))) → U100_g(X1, rcN_in_g(f(f(X1))))
rcN_in_g(f(f(X1))) → U98_g(X1, qcO_in_g(f(X1)))
qcO_in_g(f(f(X1))) → U150_g(X1, pcM_in_gg(f(f(f(f(f(f(f(f(X1)))))))), X1))
pcM_in_gg(X1, X2) → U97_gg(X1, X2, qcK_in_gg(X1, X2))
qcK_in_gg(X1, f(X2)) → U95_gg(X1, X2, rcL_in_gg(X1, f(X2)))
rcL_in_gg(X1, X2) → U148_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X2)) → U87_gg(X1, X2, qcC_in_gg(f(X1), f(X2)))
qcC_in_gg(a, b) → qcC_out_gg(a, b)
qcC_in_gg(X1, f(f(X1))) → U84_gg(X1, pcD_in_g(X1))
pcD_in_g(X1) → U137_g(X1, rcN13_in_g(X1))
rcN13_in_g(X1) → U140_g(X1, qcA_in_g(X1))
U140_g(X1, qcA_out_g(X1)) → U141_g(X1, rcN7_in_g(X1))
rcN7_in_g(X1) → U120_g(X1, qcH_in_g(X1))
qcH_in_g(f(f(X1))) → U91_g(X1, qcI_in_g(X1))
qcI_in_g(X1) → U125_g(X1, rcN10_in_g(X1))
rcN10_in_g(X1) → U142_g(X1, qcN5_in_g(X1))
qcN5_in_g(X1) → U118_g(X1, qcN6_in_g(X1))
qcN6_in_g(f(f(X1))) → U143_g(X1, qcN2_in_g(X1))
qcN2_in_g(X1) → U114_g(X1, rcN3_in_g(X1))
rcN3_in_g(X1) → U144_g(X1, qcX_in_g(X1))
qcX_in_g(X1) → U110_g(X1, qcY_in_g(X1))
qcY_in_g(f(f(X1))) → U145_g(X1, qcU_in_g(X1))
qcU_in_g(X1) → U106_g(X1, rcV_in_g(X1))
rcV_in_g(X1) → U146_g(X1, qcQ_in_g(X1))
qcQ_in_g(X1) → U102_g(X1, qcR_in_g(X1))
qcR_in_g(f(f(X1))) → U147_g(X1, pcM_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U147_g(X1, pcM_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → qcR_out_g(f(f(X1)))
U102_g(X1, qcR_out_g(X1)) → U103_g(X1, rcN_in_g(X1))
U103_g(X1, rcN_out_g(X1)) → qcQ_out_g(X1)
U146_g(X1, qcQ_out_g(X1)) → rcV_out_g(X1)
U106_g(X1, rcV_out_g(X1)) → U107_g(X1, pcP_in_g(X1))
U107_g(X1, pcP_out_g(X1)) → qcU_out_g(X1)
U145_g(X1, qcU_out_g(X1)) → qcY_out_g(f(f(X1)))
U110_g(X1, qcY_out_g(X1)) → U111_g(X1, rcS_in_g(X1))
U111_g(X1, rcS_out_g(X1)) → qcX_out_g(X1)
U144_g(X1, qcX_out_g(X1)) → rcN3_out_g(X1)
U114_g(X1, rcN3_out_g(X1)) → U115_g(X1, pcW_in_g(X1))
U115_g(X1, pcW_out_g(X1)) → qcN2_out_g(X1)
U143_g(X1, qcN2_out_g(X1)) → qcN6_out_g(f(f(X1)))
U118_g(X1, qcN6_out_g(X1)) → U119_g(X1, rcZ_in_g(X1))
U119_g(X1, rcZ_out_g(X1)) → qcN5_out_g(X1)
U142_g(X1, qcN5_out_g(X1)) → rcN10_out_g(X1)
U125_g(X1, rcN10_out_g(X1)) → U126_g(X1, pcN4_in_g(X1))
U126_g(X1, pcN4_out_g(X1)) → qcI_out_g(X1)
U91_g(X1, qcI_out_g(X1)) → qcH_out_g(f(f(X1)))
U120_g(X1, qcH_out_g(X1)) → U121_g(X1, rcN8_in_g(X1))
rcN8_in_g(f(X1)) → U124_g(X1, tcG_in_g(X1))
tcG_in_g(X1) → U94_g(X1, qcJ_in_g(X1))
qcJ_in_g(f(X1)) → U92_g(X1, qcH_in_g(f(f(X1))))
U92_g(X1, qcH_out_g(f(f(X1)))) → U93_g(X1, qcJ_in_g(X1))
U93_g(X1, qcJ_out_g(X1)) → qcJ_out_g(f(X1))
U94_g(X1, qcJ_out_g(X1)) → tcG_out_g(X1)
U124_g(X1, tcG_out_g(X1)) → rcN8_out_g(f(X1))
U121_g(X1, rcN8_out_g(X1)) → rcN7_out_g(X1)
U141_g(X1, rcN7_out_g(X1)) → rcN13_out_g(X1)
U137_g(X1, rcN13_out_g(X1)) → U138_g(X1, rcN7_in_g(X1))
U138_g(X1, rcN7_out_g(X1)) → U139_g(X1, pcB_in_g(X1))
U139_g(X1, pcB_out_g(X1)) → pcD_out_g(X1)
U84_gg(X1, pcD_out_g(X1)) → U85_gg(X1, qcA_in_g(X1))
U85_gg(X1, qcA_out_g(X1)) → qcC_out_gg(X1, f(f(X1)))
qcC_in_gg(X1, f(f(X2))) → U86_gg(X1, X2, qcE_in_gg(X1, X2))
qcE_in_gg(a, b) → U134_gg(rcN12_in_gg(a, b))
rcN12_in_gg(X1, X2) → U154_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(a, b) → U129_gg(qcC_in_gg(a, b))
U129_gg(qcC_out_gg(a, b)) → qcN11_out_gg(a, b)
qcN11_in_gg(X1, f(X2)) → U130_gg(X1, X2, qcC_in_gg(X1, f(X2)))
U130_gg(X1, X2, qcC_out_gg(X1, f(X2))) → U131_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(f(X1), f(X1)) → U132_gg(X1, qcC_in_gg(f(X1), f(X1)))
U132_gg(X1, qcC_out_gg(f(X1), f(X1))) → U133_gg(X1, tcG_in_g(X1))
U133_gg(X1, tcG_out_g(X1)) → qcN11_out_gg(f(X1), f(X1))
U131_gg(X1, X2, qcN11_out_gg(X1, X2)) → qcN11_out_gg(X1, f(X2))
U154_gg(X1, X2, qcN11_out_gg(X1, X2)) → rcN12_out_gg(X1, X2)
rcN12_in_gg(f(X1), X1) → U155_gg(X1, tcG_in_g(X1))
U155_gg(X1, tcG_out_g(X1)) → rcN12_out_gg(f(X1), X1)
U134_gg(rcN12_out_gg(a, b)) → qcE_out_gg(a, b)
qcE_in_gg(X1, f(X2)) → U135_gg(X1, X2, rcN12_in_gg(X1, f(X2)))
U135_gg(X1, X2, rcN12_out_gg(X1, f(X2))) → U136_gg(X1, X2, qcE_in_gg(X1, X2))
U136_gg(X1, X2, qcE_out_gg(X1, X2)) → qcE_out_gg(X1, f(X2))
U86_gg(X1, X2, qcE_out_gg(X1, X2)) → qcC_out_gg(X1, f(f(X2)))
U87_gg(X1, X2, qcC_out_gg(f(X1), f(X2))) → U88_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X1)) → U89_gg(X1, qcC_in_gg(f(X1), f(X1)))
U89_gg(X1, qcC_out_gg(f(X1), f(X1))) → U90_gg(X1, tcG_in_g(X1))
U90_gg(X1, tcG_out_g(X1)) → qcF_out_gg(X1, f(X1))
U88_gg(X1, X2, qcF_out_gg(X1, X2)) → qcF_out_gg(X1, f(X2))
U148_gg(X1, X2, qcF_out_gg(X1, X2)) → rcL_out_gg(X1, X2)
rcL_in_gg(X1, X1) → U149_gg(X1, tcG_in_g(X1))
U149_gg(X1, tcG_out_g(X1)) → rcL_out_gg(X1, X1)
U95_gg(X1, X2, rcL_out_gg(X1, f(X2))) → U96_gg(X1, X2, qcK_in_gg(X1, X2))
U96_gg(X1, X2, qcK_out_gg(X1, X2)) → qcK_out_gg(X1, f(X2))
U97_gg(X1, X2, qcK_out_gg(X1, X2)) → pcM_out_gg(X1, X2)
U150_g(X1, pcM_out_gg(f(f(f(f(f(f(f(f(X1)))))))), X1)) → qcO_out_g(f(f(X1)))
U98_g(X1, qcO_out_g(f(X1))) → U99_g(X1, qcF_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U99_g(X1, qcF_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → rcN_out_g(f(f(X1)))
U100_g(X1, rcN_out_g(f(f(X1)))) → U101_g(X1, qcK_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U101_g(X1, qcK_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → pcP_out_g(f(f(X1)))
U151_g(X1, pcP_out_g(f(X1))) → qcT_out_g(f(f(X1)))
U104_g(X1, qcT_out_g(f(X1))) → U105_g(X1, qcQ_in_g(X1))
U105_g(X1, qcQ_out_g(X1)) → rcS_out_g(f(f(X1)))
U108_g(X1, rcS_out_g(f(f(X1)))) → U109_g(X1, qcU_in_g(X1))
U109_g(X1, qcU_out_g(X1)) → pcW_out_g(f(f(X1)))
U152_g(X1, pcW_out_g(f(X1))) → qcN1_out_g(f(f(X1)))
U112_g(X1, qcN1_out_g(f(X1))) → U113_g(X1, qcX_in_g(X1))
U113_g(X1, qcX_out_g(X1)) → rcZ_out_g(f(f(X1)))
U116_g(X1, rcZ_out_g(f(f(X1)))) → U117_g(X1, qcN2_in_g(X1))
U117_g(X1, qcN2_out_g(X1)) → pcN4_out_g(f(f(X1)))
U153_g(X1, pcN4_out_g(f(X1))) → qcN9_out_g(f(f(X1)))
U122_g(X1, qcN9_out_g(f(X1))) → U123_g(X1, qcN5_in_g(X1))
U123_g(X1, qcN5_out_g(X1)) → rcN8_out_g(f(f(X1)))
U127_g(X1, rcN8_out_g(f(f(X1)))) → U128_g(X1, qcI_in_g(X1))
U128_g(X1, qcI_out_g(X1)) → pcB_out_g(f(f(X1)))
U83_g(X1, pcB_out_g(f(X1))) → qcA_out_g(f(X1))

Pi is empty.
We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QC_IN_GG(X1, f(f(X1))) → U72_GG(X1, qA_in_g(X1))
QC_IN_GG(X1, f(f(X1))) → QA_IN_G(X1)
QA_IN_G(f(X1)) → U1_G(X1, pB_in_g(f(X1)))
QA_IN_G(f(X1)) → PB_IN_G(f(X1))
PB_IN_G(f(X1)) → U60_G(X1, rN8_in_g(f(X1)))
PB_IN_G(f(X1)) → RN8_IN_G(f(X1))
RN8_IN_G(f(f(f(X1)))) → U53_G(X1, pN4_in_g(f(X1)))
RN8_IN_G(f(f(f(X1)))) → PN4_IN_G(f(X1))
PN4_IN_G(f(X1)) → U44_G(X1, rZ_in_g(f(X1)))
PN4_IN_G(f(X1)) → RZ_IN_G(f(X1))
RZ_IN_G(f(f(f(X1)))) → U38_G(X1, pW_in_g(f(X1)))
RZ_IN_G(f(f(f(X1)))) → PW_IN_G(f(X1))
PW_IN_G(f(X1)) → U32_G(X1, rS_in_g(f(X1)))
PW_IN_G(f(X1)) → RS_IN_G(f(X1))
RS_IN_G(f(f(f(X1)))) → U26_G(X1, pP_in_g(f(X1)))
RS_IN_G(f(f(f(X1)))) → PP_IN_G(f(X1))
PP_IN_G(f(X1)) → U20_G(X1, rN_in_g(f(X1)))
PP_IN_G(f(X1)) → RN_IN_G(f(X1))
RN_IN_G(f(f(f(X1)))) → U17_G(X1, pM_in_gg(f(f(f(f(f(f(f(f(X1)))))))), X1))
RN_IN_G(f(f(f(X1)))) → PM_IN_GG(f(f(f(f(f(f(f(f(X1)))))))), X1)
PM_IN_GG(X1, X2) → U16_GG(X1, X2, pK_in_gg(X1, X2))
PM_IN_GG(X1, X2) → PK_IN_GG(X1, X2)
PK_IN_GG(X1, X2) → U12_GG(X1, X2, pF_in_gg(X1, X2))
PK_IN_GG(X1, X2) → PF_IN_GG(X1, X2)
PF_IN_GG(X1, X2) → U2_GG(X1, X2, qC_in_gg(f(X1), X2))
PF_IN_GG(X1, X2) → QC_IN_GG(f(X1), X2)
QC_IN_GG(X1, f(f(X1))) → U73_GG(X1, qcA_in_g(X1))
U73_GG(X1, qcA_out_g(X1)) → U74_GG(X1, rN7_in_g(X1))
U73_GG(X1, qcA_out_g(X1)) → RN7_IN_G(X1)
RN7_IN_G(X1) → U50_G(X1, qH_in_g(X1))
RN7_IN_G(X1) → QH_IN_G(X1)
QH_IN_G(f(f(X1))) → U7_G(X1, pI_in_g(X1))
QH_IN_G(f(f(X1))) → PI_IN_G(X1)
PI_IN_G(X1) → U57_G(X1, pN5_in_g(X1))
PI_IN_G(X1) → PN5_IN_G(X1)
PN5_IN_G(f(f(X1))) → U47_G(X1, pN2_in_g(X1))
PN5_IN_G(f(f(X1))) → PN2_IN_G(X1)
PN2_IN_G(X1) → U41_G(X1, pX_in_g(X1))
PN2_IN_G(X1) → PX_IN_G(X1)
PX_IN_G(f(f(X1))) → U35_G(X1, pU_in_g(X1))
PX_IN_G(f(f(X1))) → PU_IN_G(X1)
PU_IN_G(X1) → U29_G(X1, pQ_in_g(X1))
PU_IN_G(X1) → PQ_IN_G(X1)
PQ_IN_G(f(f(X1))) → U23_G(X1, pM_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
PQ_IN_G(f(f(X1))) → PM_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PQ_IN_G(X1) → U24_G(X1, qcR_in_g(X1))
U24_G(X1, qcR_out_g(X1)) → U25_G(X1, rN_in_g(X1))
U24_G(X1, qcR_out_g(X1)) → RN_IN_G(X1)
RN_IN_G(f(f(X1))) → U18_G(X1, qcO_in_g(f(X1)))
U18_G(X1, qcO_out_g(f(X1))) → U19_G(X1, pF_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U18_G(X1, qcO_out_g(f(X1))) → PF_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PF_IN_GG(X1, f(X2)) → U3_GG(X1, X2, qcC_in_gg(f(X1), f(X2)))
U3_GG(X1, X2, qcC_out_gg(f(X1), f(X2))) → U4_GG(X1, X2, pF_in_gg(X1, X2))
U3_GG(X1, X2, qcC_out_gg(f(X1), f(X2))) → PF_IN_GG(X1, X2)
PF_IN_GG(X1, f(X1)) → U5_GG(X1, qcC_in_gg(f(X1), f(X1)))
U5_GG(X1, qcC_out_gg(f(X1), f(X1))) → U6_GG(X1, tG_in_g(X1))
U5_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
TG_IN_G(X1) → U11_G(X1, pJ_in_g(X1))
TG_IN_G(X1) → PJ_IN_G(X1)
PJ_IN_G(X1) → U8_G(X1, qH_in_g(f(X1)))
PJ_IN_G(X1) → QH_IN_G(f(X1))
PJ_IN_G(f(X1)) → U9_G(X1, qcH_in_g(f(f(X1))))
U9_G(X1, qcH_out_g(f(f(X1)))) → U10_G(X1, pJ_in_g(X1))
U9_G(X1, qcH_out_g(f(f(X1)))) → PJ_IN_G(X1)
PU_IN_G(X1) → U30_G(X1, rcV_in_g(X1))
U30_G(X1, rcV_out_g(X1)) → U31_G(X1, pP_in_g(X1))
U30_G(X1, rcV_out_g(X1)) → PP_IN_G(X1)
PP_IN_G(f(f(X1))) → U21_G(X1, rcN_in_g(f(f(X1))))
U21_G(X1, rcN_out_g(f(f(X1)))) → U22_G(X1, pK_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U21_G(X1, rcN_out_g(f(f(X1)))) → PK_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PK_IN_GG(X1, X1) → U13_GG(X1, tG_in_g(X1))
PK_IN_GG(X1, X1) → TG_IN_G(X1)
PK_IN_GG(X1, f(X2)) → U14_GG(X1, X2, rcL_in_gg(X1, f(X2)))
U14_GG(X1, X2, rcL_out_gg(X1, f(X2))) → U15_GG(X1, X2, pK_in_gg(X1, X2))
U14_GG(X1, X2, rcL_out_gg(X1, f(X2))) → PK_IN_GG(X1, X2)
PX_IN_G(X1) → U36_G(X1, qcY_in_g(X1))
U36_G(X1, qcY_out_g(X1)) → U37_G(X1, rS_in_g(X1))
U36_G(X1, qcY_out_g(X1)) → RS_IN_G(X1)
RS_IN_G(f(f(X1))) → U27_G(X1, qcT_in_g(f(X1)))
U27_G(X1, qcT_out_g(f(X1))) → U28_G(X1, pQ_in_g(X1))
U27_G(X1, qcT_out_g(f(X1))) → PQ_IN_G(X1)
PN2_IN_G(X1) → U42_G(X1, rcN3_in_g(X1))
U42_G(X1, rcN3_out_g(X1)) → U43_G(X1, pW_in_g(X1))
U42_G(X1, rcN3_out_g(X1)) → PW_IN_G(X1)
PW_IN_G(f(f(X1))) → U33_G(X1, rcS_in_g(f(f(X1))))
U33_G(X1, rcS_out_g(f(f(X1)))) → U34_G(X1, pU_in_g(X1))
U33_G(X1, rcS_out_g(f(f(X1)))) → PU_IN_G(X1)
PN5_IN_G(X1) → U48_G(X1, qcN6_in_g(X1))
U48_G(X1, qcN6_out_g(X1)) → U49_G(X1, rZ_in_g(X1))
U48_G(X1, qcN6_out_g(X1)) → RZ_IN_G(X1)
RZ_IN_G(f(f(X1))) → U39_G(X1, qcN1_in_g(f(X1)))
U39_G(X1, qcN1_out_g(f(X1))) → U40_G(X1, pX_in_g(X1))
U39_G(X1, qcN1_out_g(f(X1))) → PX_IN_G(X1)
PI_IN_G(X1) → U58_G(X1, rcN10_in_g(X1))
U58_G(X1, rcN10_out_g(X1)) → U59_G(X1, pN4_in_g(X1))
U58_G(X1, rcN10_out_g(X1)) → PN4_IN_G(X1)
PN4_IN_G(f(f(X1))) → U45_G(X1, rcZ_in_g(f(f(X1))))
U45_G(X1, rcZ_out_g(f(f(X1)))) → U46_G(X1, pN2_in_g(X1))
U45_G(X1, rcZ_out_g(f(f(X1)))) → PN2_IN_G(X1)
RN7_IN_G(X1) → U51_G(X1, qcH_in_g(X1))
U51_G(X1, qcH_out_g(X1)) → U52_G(X1, rN8_in_g(X1))
U51_G(X1, qcH_out_g(X1)) → RN8_IN_G(X1)
RN8_IN_G(f(f(X1))) → U54_G(X1, qcN9_in_g(f(X1)))
U54_G(X1, qcN9_out_g(f(X1))) → U55_G(X1, pN5_in_g(X1))
U54_G(X1, qcN9_out_g(f(X1))) → PN5_IN_G(X1)
RN8_IN_G(f(X1)) → U56_G(X1, tG_in_g(X1))
RN8_IN_G(f(X1)) → TG_IN_G(X1)
QC_IN_GG(X1, f(f(X1))) → U75_GG(X1, rcN13_in_g(X1))
U75_GG(X1, rcN13_out_g(X1)) → U76_GG(X1, rN7_in_g(X1))
U75_GG(X1, rcN13_out_g(X1)) → RN7_IN_G(X1)
U75_GG(X1, rcN13_out_g(X1)) → U77_GG(X1, rcN7_in_g(X1))
U77_GG(X1, rcN7_out_g(X1)) → U78_GG(X1, pB_in_g(X1))
U77_GG(X1, rcN7_out_g(X1)) → PB_IN_G(X1)
PB_IN_G(f(f(X1))) → U61_G(X1, rcN8_in_g(f(f(X1))))
U61_G(X1, rcN8_out_g(f(f(X1)))) → U62_G(X1, pI_in_g(X1))
U61_G(X1, rcN8_out_g(f(f(X1)))) → PI_IN_G(X1)
QC_IN_GG(X1, f(f(X1))) → U79_GG(X1, pcD_in_g(X1))
U79_GG(X1, pcD_out_g(X1)) → U80_GG(X1, qA_in_g(X1))
U79_GG(X1, pcD_out_g(X1)) → QA_IN_G(X1)
QC_IN_GG(X1, f(f(X2))) → U81_GG(X1, X2, pE_in_gg(X1, X2))
QC_IN_GG(X1, f(f(X2))) → PE_IN_GG(X1, X2)
PE_IN_GG(X1, X2) → U68_GG(X1, X2, pN11_in_gg(X1, X2))
PE_IN_GG(X1, X2) → PN11_IN_GG(X1, X2)
PN11_IN_GG(X1, X2) → U63_GG(X1, X2, qC_in_gg(X1, X2))
PN11_IN_GG(X1, X2) → QC_IN_GG(X1, X2)
PN11_IN_GG(X1, f(X2)) → U64_GG(X1, X2, qcC_in_gg(X1, f(X2)))
U64_GG(X1, X2, qcC_out_gg(X1, f(X2))) → U65_GG(X1, X2, pN11_in_gg(X1, X2))
U64_GG(X1, X2, qcC_out_gg(X1, f(X2))) → PN11_IN_GG(X1, X2)
PN11_IN_GG(f(X1), f(X1)) → U66_GG(X1, qcC_in_gg(f(X1), f(X1)))
U66_GG(X1, qcC_out_gg(f(X1), f(X1))) → U67_GG(X1, tG_in_g(X1))
U66_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
PE_IN_GG(f(X1), X1) → U69_GG(X1, tG_in_g(X1))
PE_IN_GG(f(X1), X1) → TG_IN_G(X1)
PE_IN_GG(X1, f(X2)) → U70_GG(X1, X2, rcN12_in_gg(X1, f(X2)))
U70_GG(X1, X2, rcN12_out_gg(X1, f(X2))) → U71_GG(X1, X2, pE_in_gg(X1, X2))
U70_GG(X1, X2, rcN12_out_gg(X1, f(X2))) → PE_IN_GG(X1, X2)

The TRS R consists of the following rules:

qcA_in_g(f(X1)) → U83_g(X1, pcB_in_g(f(X1)))
pcB_in_g(f(f(X1))) → U127_g(X1, rcN8_in_g(f(f(X1))))
rcN8_in_g(f(f(X1))) → U122_g(X1, qcN9_in_g(f(X1)))
qcN9_in_g(f(f(X1))) → U153_g(X1, pcN4_in_g(f(X1)))
pcN4_in_g(f(f(X1))) → U116_g(X1, rcZ_in_g(f(f(X1))))
rcZ_in_g(f(f(X1))) → U112_g(X1, qcN1_in_g(f(X1)))
qcN1_in_g(f(f(X1))) → U152_g(X1, pcW_in_g(f(X1)))
pcW_in_g(f(f(X1))) → U108_g(X1, rcS_in_g(f(f(X1))))
rcS_in_g(f(f(X1))) → U104_g(X1, qcT_in_g(f(X1)))
qcT_in_g(f(f(X1))) → U151_g(X1, pcP_in_g(f(X1)))
pcP_in_g(f(f(X1))) → U100_g(X1, rcN_in_g(f(f(X1))))
rcN_in_g(f(f(X1))) → U98_g(X1, qcO_in_g(f(X1)))
qcO_in_g(f(f(X1))) → U150_g(X1, pcM_in_gg(f(f(f(f(f(f(f(f(X1)))))))), X1))
pcM_in_gg(X1, X2) → U97_gg(X1, X2, qcK_in_gg(X1, X2))
qcK_in_gg(X1, f(X2)) → U95_gg(X1, X2, rcL_in_gg(X1, f(X2)))
rcL_in_gg(X1, X2) → U148_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X2)) → U87_gg(X1, X2, qcC_in_gg(f(X1), f(X2)))
qcC_in_gg(a, b) → qcC_out_gg(a, b)
qcC_in_gg(X1, f(f(X1))) → U84_gg(X1, pcD_in_g(X1))
pcD_in_g(X1) → U137_g(X1, rcN13_in_g(X1))
rcN13_in_g(X1) → U140_g(X1, qcA_in_g(X1))
U140_g(X1, qcA_out_g(X1)) → U141_g(X1, rcN7_in_g(X1))
rcN7_in_g(X1) → U120_g(X1, qcH_in_g(X1))
qcH_in_g(f(f(X1))) → U91_g(X1, qcI_in_g(X1))
qcI_in_g(X1) → U125_g(X1, rcN10_in_g(X1))
rcN10_in_g(X1) → U142_g(X1, qcN5_in_g(X1))
qcN5_in_g(X1) → U118_g(X1, qcN6_in_g(X1))
qcN6_in_g(f(f(X1))) → U143_g(X1, qcN2_in_g(X1))
qcN2_in_g(X1) → U114_g(X1, rcN3_in_g(X1))
rcN3_in_g(X1) → U144_g(X1, qcX_in_g(X1))
qcX_in_g(X1) → U110_g(X1, qcY_in_g(X1))
qcY_in_g(f(f(X1))) → U145_g(X1, qcU_in_g(X1))
qcU_in_g(X1) → U106_g(X1, rcV_in_g(X1))
rcV_in_g(X1) → U146_g(X1, qcQ_in_g(X1))
qcQ_in_g(X1) → U102_g(X1, qcR_in_g(X1))
qcR_in_g(f(f(X1))) → U147_g(X1, pcM_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U147_g(X1, pcM_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → qcR_out_g(f(f(X1)))
U102_g(X1, qcR_out_g(X1)) → U103_g(X1, rcN_in_g(X1))
U103_g(X1, rcN_out_g(X1)) → qcQ_out_g(X1)
U146_g(X1, qcQ_out_g(X1)) → rcV_out_g(X1)
U106_g(X1, rcV_out_g(X1)) → U107_g(X1, pcP_in_g(X1))
U107_g(X1, pcP_out_g(X1)) → qcU_out_g(X1)
U145_g(X1, qcU_out_g(X1)) → qcY_out_g(f(f(X1)))
U110_g(X1, qcY_out_g(X1)) → U111_g(X1, rcS_in_g(X1))
U111_g(X1, rcS_out_g(X1)) → qcX_out_g(X1)
U144_g(X1, qcX_out_g(X1)) → rcN3_out_g(X1)
U114_g(X1, rcN3_out_g(X1)) → U115_g(X1, pcW_in_g(X1))
U115_g(X1, pcW_out_g(X1)) → qcN2_out_g(X1)
U143_g(X1, qcN2_out_g(X1)) → qcN6_out_g(f(f(X1)))
U118_g(X1, qcN6_out_g(X1)) → U119_g(X1, rcZ_in_g(X1))
U119_g(X1, rcZ_out_g(X1)) → qcN5_out_g(X1)
U142_g(X1, qcN5_out_g(X1)) → rcN10_out_g(X1)
U125_g(X1, rcN10_out_g(X1)) → U126_g(X1, pcN4_in_g(X1))
U126_g(X1, pcN4_out_g(X1)) → qcI_out_g(X1)
U91_g(X1, qcI_out_g(X1)) → qcH_out_g(f(f(X1)))
U120_g(X1, qcH_out_g(X1)) → U121_g(X1, rcN8_in_g(X1))
rcN8_in_g(f(X1)) → U124_g(X1, tcG_in_g(X1))
tcG_in_g(X1) → U94_g(X1, qcJ_in_g(X1))
qcJ_in_g(f(X1)) → U92_g(X1, qcH_in_g(f(f(X1))))
U92_g(X1, qcH_out_g(f(f(X1)))) → U93_g(X1, qcJ_in_g(X1))
U93_g(X1, qcJ_out_g(X1)) → qcJ_out_g(f(X1))
U94_g(X1, qcJ_out_g(X1)) → tcG_out_g(X1)
U124_g(X1, tcG_out_g(X1)) → rcN8_out_g(f(X1))
U121_g(X1, rcN8_out_g(X1)) → rcN7_out_g(X1)
U141_g(X1, rcN7_out_g(X1)) → rcN13_out_g(X1)
U137_g(X1, rcN13_out_g(X1)) → U138_g(X1, rcN7_in_g(X1))
U138_g(X1, rcN7_out_g(X1)) → U139_g(X1, pcB_in_g(X1))
U139_g(X1, pcB_out_g(X1)) → pcD_out_g(X1)
U84_gg(X1, pcD_out_g(X1)) → U85_gg(X1, qcA_in_g(X1))
U85_gg(X1, qcA_out_g(X1)) → qcC_out_gg(X1, f(f(X1)))
qcC_in_gg(X1, f(f(X2))) → U86_gg(X1, X2, qcE_in_gg(X1, X2))
qcE_in_gg(a, b) → U134_gg(rcN12_in_gg(a, b))
rcN12_in_gg(X1, X2) → U154_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(a, b) → U129_gg(qcC_in_gg(a, b))
U129_gg(qcC_out_gg(a, b)) → qcN11_out_gg(a, b)
qcN11_in_gg(X1, f(X2)) → U130_gg(X1, X2, qcC_in_gg(X1, f(X2)))
U130_gg(X1, X2, qcC_out_gg(X1, f(X2))) → U131_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(f(X1), f(X1)) → U132_gg(X1, qcC_in_gg(f(X1), f(X1)))
U132_gg(X1, qcC_out_gg(f(X1), f(X1))) → U133_gg(X1, tcG_in_g(X1))
U133_gg(X1, tcG_out_g(X1)) → qcN11_out_gg(f(X1), f(X1))
U131_gg(X1, X2, qcN11_out_gg(X1, X2)) → qcN11_out_gg(X1, f(X2))
U154_gg(X1, X2, qcN11_out_gg(X1, X2)) → rcN12_out_gg(X1, X2)
rcN12_in_gg(f(X1), X1) → U155_gg(X1, tcG_in_g(X1))
U155_gg(X1, tcG_out_g(X1)) → rcN12_out_gg(f(X1), X1)
U134_gg(rcN12_out_gg(a, b)) → qcE_out_gg(a, b)
qcE_in_gg(X1, f(X2)) → U135_gg(X1, X2, rcN12_in_gg(X1, f(X2)))
U135_gg(X1, X2, rcN12_out_gg(X1, f(X2))) → U136_gg(X1, X2, qcE_in_gg(X1, X2))
U136_gg(X1, X2, qcE_out_gg(X1, X2)) → qcE_out_gg(X1, f(X2))
U86_gg(X1, X2, qcE_out_gg(X1, X2)) → qcC_out_gg(X1, f(f(X2)))
U87_gg(X1, X2, qcC_out_gg(f(X1), f(X2))) → U88_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X1)) → U89_gg(X1, qcC_in_gg(f(X1), f(X1)))
U89_gg(X1, qcC_out_gg(f(X1), f(X1))) → U90_gg(X1, tcG_in_g(X1))
U90_gg(X1, tcG_out_g(X1)) → qcF_out_gg(X1, f(X1))
U88_gg(X1, X2, qcF_out_gg(X1, X2)) → qcF_out_gg(X1, f(X2))
U148_gg(X1, X2, qcF_out_gg(X1, X2)) → rcL_out_gg(X1, X2)
rcL_in_gg(X1, X1) → U149_gg(X1, tcG_in_g(X1))
U149_gg(X1, tcG_out_g(X1)) → rcL_out_gg(X1, X1)
U95_gg(X1, X2, rcL_out_gg(X1, f(X2))) → U96_gg(X1, X2, qcK_in_gg(X1, X2))
U96_gg(X1, X2, qcK_out_gg(X1, X2)) → qcK_out_gg(X1, f(X2))
U97_gg(X1, X2, qcK_out_gg(X1, X2)) → pcM_out_gg(X1, X2)
U150_g(X1, pcM_out_gg(f(f(f(f(f(f(f(f(X1)))))))), X1)) → qcO_out_g(f(f(X1)))
U98_g(X1, qcO_out_g(f(X1))) → U99_g(X1, qcF_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U99_g(X1, qcF_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → rcN_out_g(f(f(X1)))
U100_g(X1, rcN_out_g(f(f(X1)))) → U101_g(X1, qcK_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U101_g(X1, qcK_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → pcP_out_g(f(f(X1)))
U151_g(X1, pcP_out_g(f(X1))) → qcT_out_g(f(f(X1)))
U104_g(X1, qcT_out_g(f(X1))) → U105_g(X1, qcQ_in_g(X1))
U105_g(X1, qcQ_out_g(X1)) → rcS_out_g(f(f(X1)))
U108_g(X1, rcS_out_g(f(f(X1)))) → U109_g(X1, qcU_in_g(X1))
U109_g(X1, qcU_out_g(X1)) → pcW_out_g(f(f(X1)))
U152_g(X1, pcW_out_g(f(X1))) → qcN1_out_g(f(f(X1)))
U112_g(X1, qcN1_out_g(f(X1))) → U113_g(X1, qcX_in_g(X1))
U113_g(X1, qcX_out_g(X1)) → rcZ_out_g(f(f(X1)))
U116_g(X1, rcZ_out_g(f(f(X1)))) → U117_g(X1, qcN2_in_g(X1))
U117_g(X1, qcN2_out_g(X1)) → pcN4_out_g(f(f(X1)))
U153_g(X1, pcN4_out_g(f(X1))) → qcN9_out_g(f(f(X1)))
U122_g(X1, qcN9_out_g(f(X1))) → U123_g(X1, qcN5_in_g(X1))
U123_g(X1, qcN5_out_g(X1)) → rcN8_out_g(f(f(X1)))
U127_g(X1, rcN8_out_g(f(f(X1)))) → U128_g(X1, qcI_in_g(X1))
U128_g(X1, qcI_out_g(X1)) → pcB_out_g(f(f(X1)))
U83_g(X1, pcB_out_g(f(X1))) → qcA_out_g(f(X1))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 55 less nodes.

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QC_IN_GG(X1, f(f(X1))) → QA_IN_G(X1)
QA_IN_G(f(X1)) → PB_IN_G(f(X1))
PB_IN_G(f(X1)) → RN8_IN_G(f(X1))
RN8_IN_G(f(f(f(X1)))) → PN4_IN_G(f(X1))
PN4_IN_G(f(X1)) → RZ_IN_G(f(X1))
RZ_IN_G(f(f(f(X1)))) → PW_IN_G(f(X1))
PW_IN_G(f(X1)) → RS_IN_G(f(X1))
RS_IN_G(f(f(f(X1)))) → PP_IN_G(f(X1))
PP_IN_G(f(X1)) → RN_IN_G(f(X1))
RN_IN_G(f(f(f(X1)))) → PM_IN_GG(f(f(f(f(f(f(f(f(X1)))))))), X1)
PM_IN_GG(X1, X2) → PK_IN_GG(X1, X2)
PK_IN_GG(X1, X2) → PF_IN_GG(X1, X2)
PF_IN_GG(X1, X2) → QC_IN_GG(f(X1), X2)
QC_IN_GG(X1, f(f(X1))) → U73_GG(X1, qcA_in_g(X1))
U73_GG(X1, qcA_out_g(X1)) → RN7_IN_G(X1)
RN7_IN_G(X1) → QH_IN_G(X1)
QH_IN_G(f(f(X1))) → PI_IN_G(X1)
PI_IN_G(X1) → PN5_IN_G(X1)
PN5_IN_G(f(f(X1))) → PN2_IN_G(X1)
PN2_IN_G(X1) → PX_IN_G(X1)
PX_IN_G(f(f(X1))) → PU_IN_G(X1)
PU_IN_G(X1) → PQ_IN_G(X1)
PQ_IN_G(f(f(X1))) → PM_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PQ_IN_G(X1) → U24_G(X1, qcR_in_g(X1))
U24_G(X1, qcR_out_g(X1)) → RN_IN_G(X1)
RN_IN_G(f(f(X1))) → U18_G(X1, qcO_in_g(f(X1)))
U18_G(X1, qcO_out_g(f(X1))) → PF_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PF_IN_GG(X1, f(X2)) → U3_GG(X1, X2, qcC_in_gg(f(X1), f(X2)))
U3_GG(X1, X2, qcC_out_gg(f(X1), f(X2))) → PF_IN_GG(X1, X2)
PF_IN_GG(X1, f(X1)) → U5_GG(X1, qcC_in_gg(f(X1), f(X1)))
U5_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
TG_IN_G(X1) → PJ_IN_G(X1)
PJ_IN_G(X1) → QH_IN_G(f(X1))
PJ_IN_G(f(X1)) → U9_G(X1, qcH_in_g(f(f(X1))))
U9_G(X1, qcH_out_g(f(f(X1)))) → PJ_IN_G(X1)
PU_IN_G(X1) → U30_G(X1, rcV_in_g(X1))
U30_G(X1, rcV_out_g(X1)) → PP_IN_G(X1)
PP_IN_G(f(f(X1))) → U21_G(X1, rcN_in_g(f(f(X1))))
U21_G(X1, rcN_out_g(f(f(X1)))) → PK_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PK_IN_GG(X1, X1) → TG_IN_G(X1)
PK_IN_GG(X1, f(X2)) → U14_GG(X1, X2, rcL_in_gg(X1, f(X2)))
U14_GG(X1, X2, rcL_out_gg(X1, f(X2))) → PK_IN_GG(X1, X2)
PX_IN_G(X1) → U36_G(X1, qcY_in_g(X1))
U36_G(X1, qcY_out_g(X1)) → RS_IN_G(X1)
RS_IN_G(f(f(X1))) → U27_G(X1, qcT_in_g(f(X1)))
U27_G(X1, qcT_out_g(f(X1))) → PQ_IN_G(X1)
PN2_IN_G(X1) → U42_G(X1, rcN3_in_g(X1))
U42_G(X1, rcN3_out_g(X1)) → PW_IN_G(X1)
PW_IN_G(f(f(X1))) → U33_G(X1, rcS_in_g(f(f(X1))))
U33_G(X1, rcS_out_g(f(f(X1)))) → PU_IN_G(X1)
PN5_IN_G(X1) → U48_G(X1, qcN6_in_g(X1))
U48_G(X1, qcN6_out_g(X1)) → RZ_IN_G(X1)
RZ_IN_G(f(f(X1))) → U39_G(X1, qcN1_in_g(f(X1)))
U39_G(X1, qcN1_out_g(f(X1))) → PX_IN_G(X1)
PI_IN_G(X1) → U58_G(X1, rcN10_in_g(X1))
U58_G(X1, rcN10_out_g(X1)) → PN4_IN_G(X1)
PN4_IN_G(f(f(X1))) → U45_G(X1, rcZ_in_g(f(f(X1))))
U45_G(X1, rcZ_out_g(f(f(X1)))) → PN2_IN_G(X1)
RN7_IN_G(X1) → U51_G(X1, qcH_in_g(X1))
U51_G(X1, qcH_out_g(X1)) → RN8_IN_G(X1)
RN8_IN_G(f(f(X1))) → U54_G(X1, qcN9_in_g(f(X1)))
U54_G(X1, qcN9_out_g(f(X1))) → PN5_IN_G(X1)
RN8_IN_G(f(X1)) → TG_IN_G(X1)
QC_IN_GG(X1, f(f(X1))) → U75_GG(X1, rcN13_in_g(X1))
U75_GG(X1, rcN13_out_g(X1)) → RN7_IN_G(X1)
U75_GG(X1, rcN13_out_g(X1)) → U77_GG(X1, rcN7_in_g(X1))
U77_GG(X1, rcN7_out_g(X1)) → PB_IN_G(X1)
PB_IN_G(f(f(X1))) → U61_G(X1, rcN8_in_g(f(f(X1))))
U61_G(X1, rcN8_out_g(f(f(X1)))) → PI_IN_G(X1)
QC_IN_GG(X1, f(f(X1))) → U79_GG(X1, pcD_in_g(X1))
U79_GG(X1, pcD_out_g(X1)) → QA_IN_G(X1)
QC_IN_GG(X1, f(f(X2))) → PE_IN_GG(X1, X2)
PE_IN_GG(X1, X2) → PN11_IN_GG(X1, X2)
PN11_IN_GG(X1, X2) → QC_IN_GG(X1, X2)
PN11_IN_GG(X1, f(X2)) → U64_GG(X1, X2, qcC_in_gg(X1, f(X2)))
U64_GG(X1, X2, qcC_out_gg(X1, f(X2))) → PN11_IN_GG(X1, X2)
PN11_IN_GG(f(X1), f(X1)) → U66_GG(X1, qcC_in_gg(f(X1), f(X1)))
U66_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
PE_IN_GG(f(X1), X1) → TG_IN_G(X1)
PE_IN_GG(X1, f(X2)) → U70_GG(X1, X2, rcN12_in_gg(X1, f(X2)))
U70_GG(X1, X2, rcN12_out_gg(X1, f(X2))) → PE_IN_GG(X1, X2)

The TRS R consists of the following rules:

qcA_in_g(f(X1)) → U83_g(X1, pcB_in_g(f(X1)))
pcB_in_g(f(f(X1))) → U127_g(X1, rcN8_in_g(f(f(X1))))
rcN8_in_g(f(f(X1))) → U122_g(X1, qcN9_in_g(f(X1)))
qcN9_in_g(f(f(X1))) → U153_g(X1, pcN4_in_g(f(X1)))
pcN4_in_g(f(f(X1))) → U116_g(X1, rcZ_in_g(f(f(X1))))
rcZ_in_g(f(f(X1))) → U112_g(X1, qcN1_in_g(f(X1)))
qcN1_in_g(f(f(X1))) → U152_g(X1, pcW_in_g(f(X1)))
pcW_in_g(f(f(X1))) → U108_g(X1, rcS_in_g(f(f(X1))))
rcS_in_g(f(f(X1))) → U104_g(X1, qcT_in_g(f(X1)))
qcT_in_g(f(f(X1))) → U151_g(X1, pcP_in_g(f(X1)))
pcP_in_g(f(f(X1))) → U100_g(X1, rcN_in_g(f(f(X1))))
rcN_in_g(f(f(X1))) → U98_g(X1, qcO_in_g(f(X1)))
qcO_in_g(f(f(X1))) → U150_g(X1, pcM_in_gg(f(f(f(f(f(f(f(f(X1)))))))), X1))
pcM_in_gg(X1, X2) → U97_gg(X1, X2, qcK_in_gg(X1, X2))
qcK_in_gg(X1, f(X2)) → U95_gg(X1, X2, rcL_in_gg(X1, f(X2)))
rcL_in_gg(X1, X2) → U148_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X2)) → U87_gg(X1, X2, qcC_in_gg(f(X1), f(X2)))
qcC_in_gg(a, b) → qcC_out_gg(a, b)
qcC_in_gg(X1, f(f(X1))) → U84_gg(X1, pcD_in_g(X1))
pcD_in_g(X1) → U137_g(X1, rcN13_in_g(X1))
rcN13_in_g(X1) → U140_g(X1, qcA_in_g(X1))
U140_g(X1, qcA_out_g(X1)) → U141_g(X1, rcN7_in_g(X1))
rcN7_in_g(X1) → U120_g(X1, qcH_in_g(X1))
qcH_in_g(f(f(X1))) → U91_g(X1, qcI_in_g(X1))
qcI_in_g(X1) → U125_g(X1, rcN10_in_g(X1))
rcN10_in_g(X1) → U142_g(X1, qcN5_in_g(X1))
qcN5_in_g(X1) → U118_g(X1, qcN6_in_g(X1))
qcN6_in_g(f(f(X1))) → U143_g(X1, qcN2_in_g(X1))
qcN2_in_g(X1) → U114_g(X1, rcN3_in_g(X1))
rcN3_in_g(X1) → U144_g(X1, qcX_in_g(X1))
qcX_in_g(X1) → U110_g(X1, qcY_in_g(X1))
qcY_in_g(f(f(X1))) → U145_g(X1, qcU_in_g(X1))
qcU_in_g(X1) → U106_g(X1, rcV_in_g(X1))
rcV_in_g(X1) → U146_g(X1, qcQ_in_g(X1))
qcQ_in_g(X1) → U102_g(X1, qcR_in_g(X1))
qcR_in_g(f(f(X1))) → U147_g(X1, pcM_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U147_g(X1, pcM_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → qcR_out_g(f(f(X1)))
U102_g(X1, qcR_out_g(X1)) → U103_g(X1, rcN_in_g(X1))
U103_g(X1, rcN_out_g(X1)) → qcQ_out_g(X1)
U146_g(X1, qcQ_out_g(X1)) → rcV_out_g(X1)
U106_g(X1, rcV_out_g(X1)) → U107_g(X1, pcP_in_g(X1))
U107_g(X1, pcP_out_g(X1)) → qcU_out_g(X1)
U145_g(X1, qcU_out_g(X1)) → qcY_out_g(f(f(X1)))
U110_g(X1, qcY_out_g(X1)) → U111_g(X1, rcS_in_g(X1))
U111_g(X1, rcS_out_g(X1)) → qcX_out_g(X1)
U144_g(X1, qcX_out_g(X1)) → rcN3_out_g(X1)
U114_g(X1, rcN3_out_g(X1)) → U115_g(X1, pcW_in_g(X1))
U115_g(X1, pcW_out_g(X1)) → qcN2_out_g(X1)
U143_g(X1, qcN2_out_g(X1)) → qcN6_out_g(f(f(X1)))
U118_g(X1, qcN6_out_g(X1)) → U119_g(X1, rcZ_in_g(X1))
U119_g(X1, rcZ_out_g(X1)) → qcN5_out_g(X1)
U142_g(X1, qcN5_out_g(X1)) → rcN10_out_g(X1)
U125_g(X1, rcN10_out_g(X1)) → U126_g(X1, pcN4_in_g(X1))
U126_g(X1, pcN4_out_g(X1)) → qcI_out_g(X1)
U91_g(X1, qcI_out_g(X1)) → qcH_out_g(f(f(X1)))
U120_g(X1, qcH_out_g(X1)) → U121_g(X1, rcN8_in_g(X1))
rcN8_in_g(f(X1)) → U124_g(X1, tcG_in_g(X1))
tcG_in_g(X1) → U94_g(X1, qcJ_in_g(X1))
qcJ_in_g(f(X1)) → U92_g(X1, qcH_in_g(f(f(X1))))
U92_g(X1, qcH_out_g(f(f(X1)))) → U93_g(X1, qcJ_in_g(X1))
U93_g(X1, qcJ_out_g(X1)) → qcJ_out_g(f(X1))
U94_g(X1, qcJ_out_g(X1)) → tcG_out_g(X1)
U124_g(X1, tcG_out_g(X1)) → rcN8_out_g(f(X1))
U121_g(X1, rcN8_out_g(X1)) → rcN7_out_g(X1)
U141_g(X1, rcN7_out_g(X1)) → rcN13_out_g(X1)
U137_g(X1, rcN13_out_g(X1)) → U138_g(X1, rcN7_in_g(X1))
U138_g(X1, rcN7_out_g(X1)) → U139_g(X1, pcB_in_g(X1))
U139_g(X1, pcB_out_g(X1)) → pcD_out_g(X1)
U84_gg(X1, pcD_out_g(X1)) → U85_gg(X1, qcA_in_g(X1))
U85_gg(X1, qcA_out_g(X1)) → qcC_out_gg(X1, f(f(X1)))
qcC_in_gg(X1, f(f(X2))) → U86_gg(X1, X2, qcE_in_gg(X1, X2))
qcE_in_gg(a, b) → U134_gg(rcN12_in_gg(a, b))
rcN12_in_gg(X1, X2) → U154_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(a, b) → U129_gg(qcC_in_gg(a, b))
U129_gg(qcC_out_gg(a, b)) → qcN11_out_gg(a, b)
qcN11_in_gg(X1, f(X2)) → U130_gg(X1, X2, qcC_in_gg(X1, f(X2)))
U130_gg(X1, X2, qcC_out_gg(X1, f(X2))) → U131_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(f(X1), f(X1)) → U132_gg(X1, qcC_in_gg(f(X1), f(X1)))
U132_gg(X1, qcC_out_gg(f(X1), f(X1))) → U133_gg(X1, tcG_in_g(X1))
U133_gg(X1, tcG_out_g(X1)) → qcN11_out_gg(f(X1), f(X1))
U131_gg(X1, X2, qcN11_out_gg(X1, X2)) → qcN11_out_gg(X1, f(X2))
U154_gg(X1, X2, qcN11_out_gg(X1, X2)) → rcN12_out_gg(X1, X2)
rcN12_in_gg(f(X1), X1) → U155_gg(X1, tcG_in_g(X1))
U155_gg(X1, tcG_out_g(X1)) → rcN12_out_gg(f(X1), X1)
U134_gg(rcN12_out_gg(a, b)) → qcE_out_gg(a, b)
qcE_in_gg(X1, f(X2)) → U135_gg(X1, X2, rcN12_in_gg(X1, f(X2)))
U135_gg(X1, X2, rcN12_out_gg(X1, f(X2))) → U136_gg(X1, X2, qcE_in_gg(X1, X2))
U136_gg(X1, X2, qcE_out_gg(X1, X2)) → qcE_out_gg(X1, f(X2))
U86_gg(X1, X2, qcE_out_gg(X1, X2)) → qcC_out_gg(X1, f(f(X2)))
U87_gg(X1, X2, qcC_out_gg(f(X1), f(X2))) → U88_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X1)) → U89_gg(X1, qcC_in_gg(f(X1), f(X1)))
U89_gg(X1, qcC_out_gg(f(X1), f(X1))) → U90_gg(X1, tcG_in_g(X1))
U90_gg(X1, tcG_out_g(X1)) → qcF_out_gg(X1, f(X1))
U88_gg(X1, X2, qcF_out_gg(X1, X2)) → qcF_out_gg(X1, f(X2))
U148_gg(X1, X2, qcF_out_gg(X1, X2)) → rcL_out_gg(X1, X2)
rcL_in_gg(X1, X1) → U149_gg(X1, tcG_in_g(X1))
U149_gg(X1, tcG_out_g(X1)) → rcL_out_gg(X1, X1)
U95_gg(X1, X2, rcL_out_gg(X1, f(X2))) → U96_gg(X1, X2, qcK_in_gg(X1, X2))
U96_gg(X1, X2, qcK_out_gg(X1, X2)) → qcK_out_gg(X1, f(X2))
U97_gg(X1, X2, qcK_out_gg(X1, X2)) → pcM_out_gg(X1, X2)
U150_g(X1, pcM_out_gg(f(f(f(f(f(f(f(f(X1)))))))), X1)) → qcO_out_g(f(f(X1)))
U98_g(X1, qcO_out_g(f(X1))) → U99_g(X1, qcF_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U99_g(X1, qcF_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → rcN_out_g(f(f(X1)))
U100_g(X1, rcN_out_g(f(f(X1)))) → U101_g(X1, qcK_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U101_g(X1, qcK_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → pcP_out_g(f(f(X1)))
U151_g(X1, pcP_out_g(f(X1))) → qcT_out_g(f(f(X1)))
U104_g(X1, qcT_out_g(f(X1))) → U105_g(X1, qcQ_in_g(X1))
U105_g(X1, qcQ_out_g(X1)) → rcS_out_g(f(f(X1)))
U108_g(X1, rcS_out_g(f(f(X1)))) → U109_g(X1, qcU_in_g(X1))
U109_g(X1, qcU_out_g(X1)) → pcW_out_g(f(f(X1)))
U152_g(X1, pcW_out_g(f(X1))) → qcN1_out_g(f(f(X1)))
U112_g(X1, qcN1_out_g(f(X1))) → U113_g(X1, qcX_in_g(X1))
U113_g(X1, qcX_out_g(X1)) → rcZ_out_g(f(f(X1)))
U116_g(X1, rcZ_out_g(f(f(X1)))) → U117_g(X1, qcN2_in_g(X1))
U117_g(X1, qcN2_out_g(X1)) → pcN4_out_g(f(f(X1)))
U153_g(X1, pcN4_out_g(f(X1))) → qcN9_out_g(f(f(X1)))
U122_g(X1, qcN9_out_g(f(X1))) → U123_g(X1, qcN5_in_g(X1))
U123_g(X1, qcN5_out_g(X1)) → rcN8_out_g(f(f(X1)))
U127_g(X1, rcN8_out_g(f(f(X1)))) → U128_g(X1, qcI_in_g(X1))
U128_g(X1, qcI_out_g(X1)) → pcB_out_g(f(f(X1)))
U83_g(X1, pcB_out_g(f(X1))) → qcA_out_g(f(X1))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(7) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QC_IN_GG(X1, f(f(X1))) → QA_IN_G(X1)
QA_IN_G(f(X1)) → PB_IN_G(f(X1))
PB_IN_G(f(X1)) → RN8_IN_G(f(X1))
RN8_IN_G(f(f(f(X1)))) → PN4_IN_G(f(X1))
PN4_IN_G(f(X1)) → RZ_IN_G(f(X1))
RZ_IN_G(f(f(f(X1)))) → PW_IN_G(f(X1))
PW_IN_G(f(X1)) → RS_IN_G(f(X1))
RS_IN_G(f(f(f(X1)))) → PP_IN_G(f(X1))
PP_IN_G(f(X1)) → RN_IN_G(f(X1))
RN_IN_G(f(f(f(X1)))) → PM_IN_GG(f(f(f(f(f(f(f(f(X1)))))))), X1)
PM_IN_GG(X1, X2) → PK_IN_GG(X1, X2)
PK_IN_GG(X1, X2) → PF_IN_GG(X1, X2)
PF_IN_GG(X1, X2) → QC_IN_GG(f(X1), X2)
QC_IN_GG(X1, f(f(X1))) → U73_GG(X1, qcA_in_g(X1))
U73_GG(X1, qcA_out_g(X1)) → RN7_IN_G(X1)
RN7_IN_G(X1) → QH_IN_G(X1)
QH_IN_G(f(f(X1))) → PI_IN_G(X1)
PI_IN_G(X1) → PN5_IN_G(X1)
PN5_IN_G(f(f(X1))) → PN2_IN_G(X1)
PN2_IN_G(X1) → PX_IN_G(X1)
PX_IN_G(f(f(X1))) → PU_IN_G(X1)
PU_IN_G(X1) → PQ_IN_G(X1)
PQ_IN_G(f(f(X1))) → PM_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PQ_IN_G(X1) → U24_G(X1, qcR_in_g(X1))
U24_G(X1, qcR_out_g(X1)) → RN_IN_G(X1)
RN_IN_G(f(f(X1))) → U18_G(X1, qcO_in_g(f(X1)))
U18_G(X1, qcO_out_g(f(X1))) → PF_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PF_IN_GG(X1, f(X2)) → U3_GG(X1, X2, qcC_in_gg(f(X1), f(X2)))
U3_GG(X1, X2, qcC_out_gg(f(X1), f(X2))) → PF_IN_GG(X1, X2)
PF_IN_GG(X1, f(X1)) → U5_GG(X1, qcC_in_gg(f(X1), f(X1)))
U5_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
TG_IN_G(X1) → PJ_IN_G(X1)
PJ_IN_G(X1) → QH_IN_G(f(X1))
PJ_IN_G(f(X1)) → U9_G(X1, qcH_in_g(f(f(X1))))
U9_G(X1, qcH_out_g(f(f(X1)))) → PJ_IN_G(X1)
PU_IN_G(X1) → U30_G(X1, rcV_in_g(X1))
U30_G(X1, rcV_out_g(X1)) → PP_IN_G(X1)
PP_IN_G(f(f(X1))) → U21_G(X1, rcN_in_g(f(f(X1))))
U21_G(X1, rcN_out_g(f(f(X1)))) → PK_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PK_IN_GG(X1, X1) → TG_IN_G(X1)
PK_IN_GG(X1, f(X2)) → U14_GG(X1, X2, rcL_in_gg(X1, f(X2)))
U14_GG(X1, X2, rcL_out_gg(X1, f(X2))) → PK_IN_GG(X1, X2)
PX_IN_G(X1) → U36_G(X1, qcY_in_g(X1))
U36_G(X1, qcY_out_g(X1)) → RS_IN_G(X1)
RS_IN_G(f(f(X1))) → U27_G(X1, qcT_in_g(f(X1)))
U27_G(X1, qcT_out_g(f(X1))) → PQ_IN_G(X1)
PN2_IN_G(X1) → U42_G(X1, rcN3_in_g(X1))
U42_G(X1, rcN3_out_g(X1)) → PW_IN_G(X1)
PW_IN_G(f(f(X1))) → U33_G(X1, rcS_in_g(f(f(X1))))
U33_G(X1, rcS_out_g(f(f(X1)))) → PU_IN_G(X1)
PN5_IN_G(X1) → U48_G(X1, qcN6_in_g(X1))
U48_G(X1, qcN6_out_g(X1)) → RZ_IN_G(X1)
RZ_IN_G(f(f(X1))) → U39_G(X1, qcN1_in_g(f(X1)))
U39_G(X1, qcN1_out_g(f(X1))) → PX_IN_G(X1)
PI_IN_G(X1) → U58_G(X1, rcN10_in_g(X1))
U58_G(X1, rcN10_out_g(X1)) → PN4_IN_G(X1)
PN4_IN_G(f(f(X1))) → U45_G(X1, rcZ_in_g(f(f(X1))))
U45_G(X1, rcZ_out_g(f(f(X1)))) → PN2_IN_G(X1)
RN7_IN_G(X1) → U51_G(X1, qcH_in_g(X1))
U51_G(X1, qcH_out_g(X1)) → RN8_IN_G(X1)
RN8_IN_G(f(f(X1))) → U54_G(X1, qcN9_in_g(f(X1)))
U54_G(X1, qcN9_out_g(f(X1))) → PN5_IN_G(X1)
RN8_IN_G(f(X1)) → TG_IN_G(X1)
QC_IN_GG(X1, f(f(X1))) → U75_GG(X1, rcN13_in_g(X1))
U75_GG(X1, rcN13_out_g(X1)) → RN7_IN_G(X1)
U75_GG(X1, rcN13_out_g(X1)) → U77_GG(X1, rcN7_in_g(X1))
U77_GG(X1, rcN7_out_g(X1)) → PB_IN_G(X1)
PB_IN_G(f(f(X1))) → U61_G(X1, rcN8_in_g(f(f(X1))))
U61_G(X1, rcN8_out_g(f(f(X1)))) → PI_IN_G(X1)
QC_IN_GG(X1, f(f(X1))) → U79_GG(X1, pcD_in_g(X1))
U79_GG(X1, pcD_out_g(X1)) → QA_IN_G(X1)
QC_IN_GG(X1, f(f(X2))) → PE_IN_GG(X1, X2)
PE_IN_GG(X1, X2) → PN11_IN_GG(X1, X2)
PN11_IN_GG(X1, X2) → QC_IN_GG(X1, X2)
PN11_IN_GG(X1, f(X2)) → U64_GG(X1, X2, qcC_in_gg(X1, f(X2)))
U64_GG(X1, X2, qcC_out_gg(X1, f(X2))) → PN11_IN_GG(X1, X2)
PN11_IN_GG(f(X1), f(X1)) → U66_GG(X1, qcC_in_gg(f(X1), f(X1)))
U66_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
PE_IN_GG(f(X1), X1) → TG_IN_G(X1)
PE_IN_GG(X1, f(X2)) → U70_GG(X1, X2, rcN12_in_gg(X1, f(X2)))
U70_GG(X1, X2, rcN12_out_gg(X1, f(X2))) → PE_IN_GG(X1, X2)

The TRS R consists of the following rules:

qcA_in_g(f(X1)) → U83_g(X1, pcB_in_g(f(X1)))
pcB_in_g(f(f(X1))) → U127_g(X1, rcN8_in_g(f(f(X1))))
rcN8_in_g(f(f(X1))) → U122_g(X1, qcN9_in_g(f(X1)))
qcN9_in_g(f(f(X1))) → U153_g(X1, pcN4_in_g(f(X1)))
pcN4_in_g(f(f(X1))) → U116_g(X1, rcZ_in_g(f(f(X1))))
rcZ_in_g(f(f(X1))) → U112_g(X1, qcN1_in_g(f(X1)))
qcN1_in_g(f(f(X1))) → U152_g(X1, pcW_in_g(f(X1)))
pcW_in_g(f(f(X1))) → U108_g(X1, rcS_in_g(f(f(X1))))
rcS_in_g(f(f(X1))) → U104_g(X1, qcT_in_g(f(X1)))
qcT_in_g(f(f(X1))) → U151_g(X1, pcP_in_g(f(X1)))
pcP_in_g(f(f(X1))) → U100_g(X1, rcN_in_g(f(f(X1))))
rcN_in_g(f(f(X1))) → U98_g(X1, qcO_in_g(f(X1)))
qcO_in_g(f(f(X1))) → U150_g(X1, pcM_in_gg(f(f(f(f(f(f(f(f(X1)))))))), X1))
pcM_in_gg(X1, X2) → U97_gg(X1, X2, qcK_in_gg(X1, X2))
qcK_in_gg(X1, f(X2)) → U95_gg(X1, X2, rcL_in_gg(X1, f(X2)))
rcL_in_gg(X1, X2) → U148_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X2)) → U87_gg(X1, X2, qcC_in_gg(f(X1), f(X2)))
qcC_in_gg(a, b) → qcC_out_gg(a, b)
qcC_in_gg(X1, f(f(X1))) → U84_gg(X1, pcD_in_g(X1))
pcD_in_g(X1) → U137_g(X1, rcN13_in_g(X1))
rcN13_in_g(X1) → U140_g(X1, qcA_in_g(X1))
U140_g(X1, qcA_out_g(X1)) → U141_g(X1, rcN7_in_g(X1))
rcN7_in_g(X1) → U120_g(X1, qcH_in_g(X1))
qcH_in_g(f(f(X1))) → U91_g(X1, qcI_in_g(X1))
qcI_in_g(X1) → U125_g(X1, rcN10_in_g(X1))
rcN10_in_g(X1) → U142_g(X1, qcN5_in_g(X1))
qcN5_in_g(X1) → U118_g(X1, qcN6_in_g(X1))
qcN6_in_g(f(f(X1))) → U143_g(X1, qcN2_in_g(X1))
qcN2_in_g(X1) → U114_g(X1, rcN3_in_g(X1))
rcN3_in_g(X1) → U144_g(X1, qcX_in_g(X1))
qcX_in_g(X1) → U110_g(X1, qcY_in_g(X1))
qcY_in_g(f(f(X1))) → U145_g(X1, qcU_in_g(X1))
qcU_in_g(X1) → U106_g(X1, rcV_in_g(X1))
rcV_in_g(X1) → U146_g(X1, qcQ_in_g(X1))
qcQ_in_g(X1) → U102_g(X1, qcR_in_g(X1))
qcR_in_g(f(f(X1))) → U147_g(X1, pcM_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U147_g(X1, pcM_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → qcR_out_g(f(f(X1)))
U102_g(X1, qcR_out_g(X1)) → U103_g(X1, rcN_in_g(X1))
U103_g(X1, rcN_out_g(X1)) → qcQ_out_g(X1)
U146_g(X1, qcQ_out_g(X1)) → rcV_out_g(X1)
U106_g(X1, rcV_out_g(X1)) → U107_g(X1, pcP_in_g(X1))
U107_g(X1, pcP_out_g(X1)) → qcU_out_g(X1)
U145_g(X1, qcU_out_g(X1)) → qcY_out_g(f(f(X1)))
U110_g(X1, qcY_out_g(X1)) → U111_g(X1, rcS_in_g(X1))
U111_g(X1, rcS_out_g(X1)) → qcX_out_g(X1)
U144_g(X1, qcX_out_g(X1)) → rcN3_out_g(X1)
U114_g(X1, rcN3_out_g(X1)) → U115_g(X1, pcW_in_g(X1))
U115_g(X1, pcW_out_g(X1)) → qcN2_out_g(X1)
U143_g(X1, qcN2_out_g(X1)) → qcN6_out_g(f(f(X1)))
U118_g(X1, qcN6_out_g(X1)) → U119_g(X1, rcZ_in_g(X1))
U119_g(X1, rcZ_out_g(X1)) → qcN5_out_g(X1)
U142_g(X1, qcN5_out_g(X1)) → rcN10_out_g(X1)
U125_g(X1, rcN10_out_g(X1)) → U126_g(X1, pcN4_in_g(X1))
U126_g(X1, pcN4_out_g(X1)) → qcI_out_g(X1)
U91_g(X1, qcI_out_g(X1)) → qcH_out_g(f(f(X1)))
U120_g(X1, qcH_out_g(X1)) → U121_g(X1, rcN8_in_g(X1))
rcN8_in_g(f(X1)) → U124_g(X1, tcG_in_g(X1))
tcG_in_g(X1) → U94_g(X1, qcJ_in_g(X1))
qcJ_in_g(f(X1)) → U92_g(X1, qcH_in_g(f(f(X1))))
U92_g(X1, qcH_out_g(f(f(X1)))) → U93_g(X1, qcJ_in_g(X1))
U93_g(X1, qcJ_out_g(X1)) → qcJ_out_g(f(X1))
U94_g(X1, qcJ_out_g(X1)) → tcG_out_g(X1)
U124_g(X1, tcG_out_g(X1)) → rcN8_out_g(f(X1))
U121_g(X1, rcN8_out_g(X1)) → rcN7_out_g(X1)
U141_g(X1, rcN7_out_g(X1)) → rcN13_out_g(X1)
U137_g(X1, rcN13_out_g(X1)) → U138_g(X1, rcN7_in_g(X1))
U138_g(X1, rcN7_out_g(X1)) → U139_g(X1, pcB_in_g(X1))
U139_g(X1, pcB_out_g(X1)) → pcD_out_g(X1)
U84_gg(X1, pcD_out_g(X1)) → U85_gg(X1, qcA_in_g(X1))
U85_gg(X1, qcA_out_g(X1)) → qcC_out_gg(X1, f(f(X1)))
qcC_in_gg(X1, f(f(X2))) → U86_gg(X1, X2, qcE_in_gg(X1, X2))
qcE_in_gg(a, b) → U134_gg(rcN12_in_gg(a, b))
rcN12_in_gg(X1, X2) → U154_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(a, b) → U129_gg(qcC_in_gg(a, b))
U129_gg(qcC_out_gg(a, b)) → qcN11_out_gg(a, b)
qcN11_in_gg(X1, f(X2)) → U130_gg(X1, X2, qcC_in_gg(X1, f(X2)))
U130_gg(X1, X2, qcC_out_gg(X1, f(X2))) → U131_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(f(X1), f(X1)) → U132_gg(X1, qcC_in_gg(f(X1), f(X1)))
U132_gg(X1, qcC_out_gg(f(X1), f(X1))) → U133_gg(X1, tcG_in_g(X1))
U133_gg(X1, tcG_out_g(X1)) → qcN11_out_gg(f(X1), f(X1))
U131_gg(X1, X2, qcN11_out_gg(X1, X2)) → qcN11_out_gg(X1, f(X2))
U154_gg(X1, X2, qcN11_out_gg(X1, X2)) → rcN12_out_gg(X1, X2)
rcN12_in_gg(f(X1), X1) → U155_gg(X1, tcG_in_g(X1))
U155_gg(X1, tcG_out_g(X1)) → rcN12_out_gg(f(X1), X1)
U134_gg(rcN12_out_gg(a, b)) → qcE_out_gg(a, b)
qcE_in_gg(X1, f(X2)) → U135_gg(X1, X2, rcN12_in_gg(X1, f(X2)))
U135_gg(X1, X2, rcN12_out_gg(X1, f(X2))) → U136_gg(X1, X2, qcE_in_gg(X1, X2))
U136_gg(X1, X2, qcE_out_gg(X1, X2)) → qcE_out_gg(X1, f(X2))
U86_gg(X1, X2, qcE_out_gg(X1, X2)) → qcC_out_gg(X1, f(f(X2)))
U87_gg(X1, X2, qcC_out_gg(f(X1), f(X2))) → U88_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X1)) → U89_gg(X1, qcC_in_gg(f(X1), f(X1)))
U89_gg(X1, qcC_out_gg(f(X1), f(X1))) → U90_gg(X1, tcG_in_g(X1))
U90_gg(X1, tcG_out_g(X1)) → qcF_out_gg(X1, f(X1))
U88_gg(X1, X2, qcF_out_gg(X1, X2)) → qcF_out_gg(X1, f(X2))
U148_gg(X1, X2, qcF_out_gg(X1, X2)) → rcL_out_gg(X1, X2)
rcL_in_gg(X1, X1) → U149_gg(X1, tcG_in_g(X1))
U149_gg(X1, tcG_out_g(X1)) → rcL_out_gg(X1, X1)
U95_gg(X1, X2, rcL_out_gg(X1, f(X2))) → U96_gg(X1, X2, qcK_in_gg(X1, X2))
U96_gg(X1, X2, qcK_out_gg(X1, X2)) → qcK_out_gg(X1, f(X2))
U97_gg(X1, X2, qcK_out_gg(X1, X2)) → pcM_out_gg(X1, X2)
U150_g(X1, pcM_out_gg(f(f(f(f(f(f(f(f(X1)))))))), X1)) → qcO_out_g(f(f(X1)))
U98_g(X1, qcO_out_g(f(X1))) → U99_g(X1, qcF_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U99_g(X1, qcF_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → rcN_out_g(f(f(X1)))
U100_g(X1, rcN_out_g(f(f(X1)))) → U101_g(X1, qcK_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U101_g(X1, qcK_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → pcP_out_g(f(f(X1)))
U151_g(X1, pcP_out_g(f(X1))) → qcT_out_g(f(f(X1)))
U104_g(X1, qcT_out_g(f(X1))) → U105_g(X1, qcQ_in_g(X1))
U105_g(X1, qcQ_out_g(X1)) → rcS_out_g(f(f(X1)))
U108_g(X1, rcS_out_g(f(f(X1)))) → U109_g(X1, qcU_in_g(X1))
U109_g(X1, qcU_out_g(X1)) → pcW_out_g(f(f(X1)))
U152_g(X1, pcW_out_g(f(X1))) → qcN1_out_g(f(f(X1)))
U112_g(X1, qcN1_out_g(f(X1))) → U113_g(X1, qcX_in_g(X1))
U113_g(X1, qcX_out_g(X1)) → rcZ_out_g(f(f(X1)))
U116_g(X1, rcZ_out_g(f(f(X1)))) → U117_g(X1, qcN2_in_g(X1))
U117_g(X1, qcN2_out_g(X1)) → pcN4_out_g(f(f(X1)))
U153_g(X1, pcN4_out_g(f(X1))) → qcN9_out_g(f(f(X1)))
U122_g(X1, qcN9_out_g(f(X1))) → U123_g(X1, qcN5_in_g(X1))
U123_g(X1, qcN5_out_g(X1)) → rcN8_out_g(f(f(X1)))
U127_g(X1, rcN8_out_g(f(f(X1)))) → U128_g(X1, qcI_in_g(X1))
U128_g(X1, qcI_out_g(X1)) → pcB_out_g(f(f(X1)))
U83_g(X1, pcB_out_g(f(X1))) → qcA_out_g(f(X1))

The set Q consists of the following terms:

qcA_in_g(x0)
pcB_in_g(x0)
rcN8_in_g(x0)
qcN9_in_g(x0)
pcN4_in_g(x0)
rcZ_in_g(x0)
qcN1_in_g(x0)
pcW_in_g(x0)
rcS_in_g(x0)
qcT_in_g(x0)
pcP_in_g(x0)
rcN_in_g(x0)
qcO_in_g(x0)
pcM_in_gg(x0, x1)
qcK_in_gg(x0, x1)
rcL_in_gg(x0, x1)
qcF_in_gg(x0, x1)
qcC_in_gg(x0, x1)
pcD_in_g(x0)
rcN13_in_g(x0)
U140_g(x0, x1)
rcN7_in_g(x0)
qcH_in_g(x0)
qcI_in_g(x0)
rcN10_in_g(x0)
qcN5_in_g(x0)
qcN6_in_g(x0)
qcN2_in_g(x0)
rcN3_in_g(x0)
qcX_in_g(x0)
qcY_in_g(x0)
qcU_in_g(x0)
rcV_in_g(x0)
qcQ_in_g(x0)
qcR_in_g(x0)
U147_g(x0, x1)
U102_g(x0, x1)
U103_g(x0, x1)
U146_g(x0, x1)
U106_g(x0, x1)
U107_g(x0, x1)
U145_g(x0, x1)
U110_g(x0, x1)
U111_g(x0, x1)
U144_g(x0, x1)
U114_g(x0, x1)
U115_g(x0, x1)
U143_g(x0, x1)
U118_g(x0, x1)
U119_g(x0, x1)
U142_g(x0, x1)
U125_g(x0, x1)
U126_g(x0, x1)
U91_g(x0, x1)
U120_g(x0, x1)
tcG_in_g(x0)
qcJ_in_g(x0)
U92_g(x0, x1)
U93_g(x0, x1)
U94_g(x0, x1)
U124_g(x0, x1)
U121_g(x0, x1)
U141_g(x0, x1)
U137_g(x0, x1)
U138_g(x0, x1)
U139_g(x0, x1)
U84_gg(x0, x1)
U85_gg(x0, x1)
qcE_in_gg(x0, x1)
rcN12_in_gg(x0, x1)
qcN11_in_gg(x0, x1)
U129_gg(x0)
U130_gg(x0, x1, x2)
U132_gg(x0, x1)
U133_gg(x0, x1)
U131_gg(x0, x1, x2)
U154_gg(x0, x1, x2)
U155_gg(x0, x1)
U134_gg(x0)
U135_gg(x0, x1, x2)
U136_gg(x0, x1, x2)
U86_gg(x0, x1, x2)
U87_gg(x0, x1, x2)
U89_gg(x0, x1)
U90_gg(x0, x1)
U88_gg(x0, x1, x2)
U148_gg(x0, x1, x2)
U149_gg(x0, x1)
U95_gg(x0, x1, x2)
U96_gg(x0, x1, x2)
U97_gg(x0, x1, x2)
U150_g(x0, x1)
U98_g(x0, x1)
U99_g(x0, x1)
U100_g(x0, x1)
U101_g(x0, x1)
U151_g(x0, x1)
U104_g(x0, x1)
U105_g(x0, x1)
U108_g(x0, x1)
U109_g(x0, x1)
U152_g(x0, x1)
U112_g(x0, x1)
U113_g(x0, x1)
U116_g(x0, x1)
U117_g(x0, x1)
U153_g(x0, x1)
U122_g(x0, x1)
U123_g(x0, x1)
U127_g(x0, x1)
U128_g(x0, x1)
U83_g(x0, x1)

We have to consider all (P,Q,R)-chains.

(9) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule PM_IN_GG(X1, X2) → PK_IN_GG(X1, X2) we obtained the following new rules [LPAR04]:

PM_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0) → PK_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0)
PM_IN_GG(f(f(f(f(f(f(f(z0))))))), z0) → PK_IN_GG(f(f(f(f(f(f(f(z0))))))), z0)

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QC_IN_GG(X1, f(f(X1))) → QA_IN_G(X1)
QA_IN_G(f(X1)) → PB_IN_G(f(X1))
PB_IN_G(f(X1)) → RN8_IN_G(f(X1))
RN8_IN_G(f(f(f(X1)))) → PN4_IN_G(f(X1))
PN4_IN_G(f(X1)) → RZ_IN_G(f(X1))
RZ_IN_G(f(f(f(X1)))) → PW_IN_G(f(X1))
PW_IN_G(f(X1)) → RS_IN_G(f(X1))
RS_IN_G(f(f(f(X1)))) → PP_IN_G(f(X1))
PP_IN_G(f(X1)) → RN_IN_G(f(X1))
RN_IN_G(f(f(f(X1)))) → PM_IN_GG(f(f(f(f(f(f(f(f(X1)))))))), X1)
PK_IN_GG(X1, X2) → PF_IN_GG(X1, X2)
PF_IN_GG(X1, X2) → QC_IN_GG(f(X1), X2)
QC_IN_GG(X1, f(f(X1))) → U73_GG(X1, qcA_in_g(X1))
U73_GG(X1, qcA_out_g(X1)) → RN7_IN_G(X1)
RN7_IN_G(X1) → QH_IN_G(X1)
QH_IN_G(f(f(X1))) → PI_IN_G(X1)
PI_IN_G(X1) → PN5_IN_G(X1)
PN5_IN_G(f(f(X1))) → PN2_IN_G(X1)
PN2_IN_G(X1) → PX_IN_G(X1)
PX_IN_G(f(f(X1))) → PU_IN_G(X1)
PU_IN_G(X1) → PQ_IN_G(X1)
PQ_IN_G(f(f(X1))) → PM_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PQ_IN_G(X1) → U24_G(X1, qcR_in_g(X1))
U24_G(X1, qcR_out_g(X1)) → RN_IN_G(X1)
RN_IN_G(f(f(X1))) → U18_G(X1, qcO_in_g(f(X1)))
U18_G(X1, qcO_out_g(f(X1))) → PF_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PF_IN_GG(X1, f(X2)) → U3_GG(X1, X2, qcC_in_gg(f(X1), f(X2)))
U3_GG(X1, X2, qcC_out_gg(f(X1), f(X2))) → PF_IN_GG(X1, X2)
PF_IN_GG(X1, f(X1)) → U5_GG(X1, qcC_in_gg(f(X1), f(X1)))
U5_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
TG_IN_G(X1) → PJ_IN_G(X1)
PJ_IN_G(X1) → QH_IN_G(f(X1))
PJ_IN_G(f(X1)) → U9_G(X1, qcH_in_g(f(f(X1))))
U9_G(X1, qcH_out_g(f(f(X1)))) → PJ_IN_G(X1)
PU_IN_G(X1) → U30_G(X1, rcV_in_g(X1))
U30_G(X1, rcV_out_g(X1)) → PP_IN_G(X1)
PP_IN_G(f(f(X1))) → U21_G(X1, rcN_in_g(f(f(X1))))
U21_G(X1, rcN_out_g(f(f(X1)))) → PK_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PK_IN_GG(X1, X1) → TG_IN_G(X1)
PK_IN_GG(X1, f(X2)) → U14_GG(X1, X2, rcL_in_gg(X1, f(X2)))
U14_GG(X1, X2, rcL_out_gg(X1, f(X2))) → PK_IN_GG(X1, X2)
PX_IN_G(X1) → U36_G(X1, qcY_in_g(X1))
U36_G(X1, qcY_out_g(X1)) → RS_IN_G(X1)
RS_IN_G(f(f(X1))) → U27_G(X1, qcT_in_g(f(X1)))
U27_G(X1, qcT_out_g(f(X1))) → PQ_IN_G(X1)
PN2_IN_G(X1) → U42_G(X1, rcN3_in_g(X1))
U42_G(X1, rcN3_out_g(X1)) → PW_IN_G(X1)
PW_IN_G(f(f(X1))) → U33_G(X1, rcS_in_g(f(f(X1))))
U33_G(X1, rcS_out_g(f(f(X1)))) → PU_IN_G(X1)
PN5_IN_G(X1) → U48_G(X1, qcN6_in_g(X1))
U48_G(X1, qcN6_out_g(X1)) → RZ_IN_G(X1)
RZ_IN_G(f(f(X1))) → U39_G(X1, qcN1_in_g(f(X1)))
U39_G(X1, qcN1_out_g(f(X1))) → PX_IN_G(X1)
PI_IN_G(X1) → U58_G(X1, rcN10_in_g(X1))
U58_G(X1, rcN10_out_g(X1)) → PN4_IN_G(X1)
PN4_IN_G(f(f(X1))) → U45_G(X1, rcZ_in_g(f(f(X1))))
U45_G(X1, rcZ_out_g(f(f(X1)))) → PN2_IN_G(X1)
RN7_IN_G(X1) → U51_G(X1, qcH_in_g(X1))
U51_G(X1, qcH_out_g(X1)) → RN8_IN_G(X1)
RN8_IN_G(f(f(X1))) → U54_G(X1, qcN9_in_g(f(X1)))
U54_G(X1, qcN9_out_g(f(X1))) → PN5_IN_G(X1)
RN8_IN_G(f(X1)) → TG_IN_G(X1)
QC_IN_GG(X1, f(f(X1))) → U75_GG(X1, rcN13_in_g(X1))
U75_GG(X1, rcN13_out_g(X1)) → RN7_IN_G(X1)
U75_GG(X1, rcN13_out_g(X1)) → U77_GG(X1, rcN7_in_g(X1))
U77_GG(X1, rcN7_out_g(X1)) → PB_IN_G(X1)
PB_IN_G(f(f(X1))) → U61_G(X1, rcN8_in_g(f(f(X1))))
U61_G(X1, rcN8_out_g(f(f(X1)))) → PI_IN_G(X1)
QC_IN_GG(X1, f(f(X1))) → U79_GG(X1, pcD_in_g(X1))
U79_GG(X1, pcD_out_g(X1)) → QA_IN_G(X1)
QC_IN_GG(X1, f(f(X2))) → PE_IN_GG(X1, X2)
PE_IN_GG(X1, X2) → PN11_IN_GG(X1, X2)
PN11_IN_GG(X1, X2) → QC_IN_GG(X1, X2)
PN11_IN_GG(X1, f(X2)) → U64_GG(X1, X2, qcC_in_gg(X1, f(X2)))
U64_GG(X1, X2, qcC_out_gg(X1, f(X2))) → PN11_IN_GG(X1, X2)
PN11_IN_GG(f(X1), f(X1)) → U66_GG(X1, qcC_in_gg(f(X1), f(X1)))
U66_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
PE_IN_GG(f(X1), X1) → TG_IN_G(X1)
PE_IN_GG(X1, f(X2)) → U70_GG(X1, X2, rcN12_in_gg(X1, f(X2)))
U70_GG(X1, X2, rcN12_out_gg(X1, f(X2))) → PE_IN_GG(X1, X2)
PM_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0) → PK_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0)
PM_IN_GG(f(f(f(f(f(f(f(z0))))))), z0) → PK_IN_GG(f(f(f(f(f(f(f(z0))))))), z0)

The TRS R consists of the following rules:

qcA_in_g(f(X1)) → U83_g(X1, pcB_in_g(f(X1)))
pcB_in_g(f(f(X1))) → U127_g(X1, rcN8_in_g(f(f(X1))))
rcN8_in_g(f(f(X1))) → U122_g(X1, qcN9_in_g(f(X1)))
qcN9_in_g(f(f(X1))) → U153_g(X1, pcN4_in_g(f(X1)))
pcN4_in_g(f(f(X1))) → U116_g(X1, rcZ_in_g(f(f(X1))))
rcZ_in_g(f(f(X1))) → U112_g(X1, qcN1_in_g(f(X1)))
qcN1_in_g(f(f(X1))) → U152_g(X1, pcW_in_g(f(X1)))
pcW_in_g(f(f(X1))) → U108_g(X1, rcS_in_g(f(f(X1))))
rcS_in_g(f(f(X1))) → U104_g(X1, qcT_in_g(f(X1)))
qcT_in_g(f(f(X1))) → U151_g(X1, pcP_in_g(f(X1)))
pcP_in_g(f(f(X1))) → U100_g(X1, rcN_in_g(f(f(X1))))
rcN_in_g(f(f(X1))) → U98_g(X1, qcO_in_g(f(X1)))
qcO_in_g(f(f(X1))) → U150_g(X1, pcM_in_gg(f(f(f(f(f(f(f(f(X1)))))))), X1))
pcM_in_gg(X1, X2) → U97_gg(X1, X2, qcK_in_gg(X1, X2))
qcK_in_gg(X1, f(X2)) → U95_gg(X1, X2, rcL_in_gg(X1, f(X2)))
rcL_in_gg(X1, X2) → U148_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X2)) → U87_gg(X1, X2, qcC_in_gg(f(X1), f(X2)))
qcC_in_gg(a, b) → qcC_out_gg(a, b)
qcC_in_gg(X1, f(f(X1))) → U84_gg(X1, pcD_in_g(X1))
pcD_in_g(X1) → U137_g(X1, rcN13_in_g(X1))
rcN13_in_g(X1) → U140_g(X1, qcA_in_g(X1))
U140_g(X1, qcA_out_g(X1)) → U141_g(X1, rcN7_in_g(X1))
rcN7_in_g(X1) → U120_g(X1, qcH_in_g(X1))
qcH_in_g(f(f(X1))) → U91_g(X1, qcI_in_g(X1))
qcI_in_g(X1) → U125_g(X1, rcN10_in_g(X1))
rcN10_in_g(X1) → U142_g(X1, qcN5_in_g(X1))
qcN5_in_g(X1) → U118_g(X1, qcN6_in_g(X1))
qcN6_in_g(f(f(X1))) → U143_g(X1, qcN2_in_g(X1))
qcN2_in_g(X1) → U114_g(X1, rcN3_in_g(X1))
rcN3_in_g(X1) → U144_g(X1, qcX_in_g(X1))
qcX_in_g(X1) → U110_g(X1, qcY_in_g(X1))
qcY_in_g(f(f(X1))) → U145_g(X1, qcU_in_g(X1))
qcU_in_g(X1) → U106_g(X1, rcV_in_g(X1))
rcV_in_g(X1) → U146_g(X1, qcQ_in_g(X1))
qcQ_in_g(X1) → U102_g(X1, qcR_in_g(X1))
qcR_in_g(f(f(X1))) → U147_g(X1, pcM_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U147_g(X1, pcM_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → qcR_out_g(f(f(X1)))
U102_g(X1, qcR_out_g(X1)) → U103_g(X1, rcN_in_g(X1))
U103_g(X1, rcN_out_g(X1)) → qcQ_out_g(X1)
U146_g(X1, qcQ_out_g(X1)) → rcV_out_g(X1)
U106_g(X1, rcV_out_g(X1)) → U107_g(X1, pcP_in_g(X1))
U107_g(X1, pcP_out_g(X1)) → qcU_out_g(X1)
U145_g(X1, qcU_out_g(X1)) → qcY_out_g(f(f(X1)))
U110_g(X1, qcY_out_g(X1)) → U111_g(X1, rcS_in_g(X1))
U111_g(X1, rcS_out_g(X1)) → qcX_out_g(X1)
U144_g(X1, qcX_out_g(X1)) → rcN3_out_g(X1)
U114_g(X1, rcN3_out_g(X1)) → U115_g(X1, pcW_in_g(X1))
U115_g(X1, pcW_out_g(X1)) → qcN2_out_g(X1)
U143_g(X1, qcN2_out_g(X1)) → qcN6_out_g(f(f(X1)))
U118_g(X1, qcN6_out_g(X1)) → U119_g(X1, rcZ_in_g(X1))
U119_g(X1, rcZ_out_g(X1)) → qcN5_out_g(X1)
U142_g(X1, qcN5_out_g(X1)) → rcN10_out_g(X1)
U125_g(X1, rcN10_out_g(X1)) → U126_g(X1, pcN4_in_g(X1))
U126_g(X1, pcN4_out_g(X1)) → qcI_out_g(X1)
U91_g(X1, qcI_out_g(X1)) → qcH_out_g(f(f(X1)))
U120_g(X1, qcH_out_g(X1)) → U121_g(X1, rcN8_in_g(X1))
rcN8_in_g(f(X1)) → U124_g(X1, tcG_in_g(X1))
tcG_in_g(X1) → U94_g(X1, qcJ_in_g(X1))
qcJ_in_g(f(X1)) → U92_g(X1, qcH_in_g(f(f(X1))))
U92_g(X1, qcH_out_g(f(f(X1)))) → U93_g(X1, qcJ_in_g(X1))
U93_g(X1, qcJ_out_g(X1)) → qcJ_out_g(f(X1))
U94_g(X1, qcJ_out_g(X1)) → tcG_out_g(X1)
U124_g(X1, tcG_out_g(X1)) → rcN8_out_g(f(X1))
U121_g(X1, rcN8_out_g(X1)) → rcN7_out_g(X1)
U141_g(X1, rcN7_out_g(X1)) → rcN13_out_g(X1)
U137_g(X1, rcN13_out_g(X1)) → U138_g(X1, rcN7_in_g(X1))
U138_g(X1, rcN7_out_g(X1)) → U139_g(X1, pcB_in_g(X1))
U139_g(X1, pcB_out_g(X1)) → pcD_out_g(X1)
U84_gg(X1, pcD_out_g(X1)) → U85_gg(X1, qcA_in_g(X1))
U85_gg(X1, qcA_out_g(X1)) → qcC_out_gg(X1, f(f(X1)))
qcC_in_gg(X1, f(f(X2))) → U86_gg(X1, X2, qcE_in_gg(X1, X2))
qcE_in_gg(a, b) → U134_gg(rcN12_in_gg(a, b))
rcN12_in_gg(X1, X2) → U154_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(a, b) → U129_gg(qcC_in_gg(a, b))
U129_gg(qcC_out_gg(a, b)) → qcN11_out_gg(a, b)
qcN11_in_gg(X1, f(X2)) → U130_gg(X1, X2, qcC_in_gg(X1, f(X2)))
U130_gg(X1, X2, qcC_out_gg(X1, f(X2))) → U131_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(f(X1), f(X1)) → U132_gg(X1, qcC_in_gg(f(X1), f(X1)))
U132_gg(X1, qcC_out_gg(f(X1), f(X1))) → U133_gg(X1, tcG_in_g(X1))
U133_gg(X1, tcG_out_g(X1)) → qcN11_out_gg(f(X1), f(X1))
U131_gg(X1, X2, qcN11_out_gg(X1, X2)) → qcN11_out_gg(X1, f(X2))
U154_gg(X1, X2, qcN11_out_gg(X1, X2)) → rcN12_out_gg(X1, X2)
rcN12_in_gg(f(X1), X1) → U155_gg(X1, tcG_in_g(X1))
U155_gg(X1, tcG_out_g(X1)) → rcN12_out_gg(f(X1), X1)
U134_gg(rcN12_out_gg(a, b)) → qcE_out_gg(a, b)
qcE_in_gg(X1, f(X2)) → U135_gg(X1, X2, rcN12_in_gg(X1, f(X2)))
U135_gg(X1, X2, rcN12_out_gg(X1, f(X2))) → U136_gg(X1, X2, qcE_in_gg(X1, X2))
U136_gg(X1, X2, qcE_out_gg(X1, X2)) → qcE_out_gg(X1, f(X2))
U86_gg(X1, X2, qcE_out_gg(X1, X2)) → qcC_out_gg(X1, f(f(X2)))
U87_gg(X1, X2, qcC_out_gg(f(X1), f(X2))) → U88_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X1)) → U89_gg(X1, qcC_in_gg(f(X1), f(X1)))
U89_gg(X1, qcC_out_gg(f(X1), f(X1))) → U90_gg(X1, tcG_in_g(X1))
U90_gg(X1, tcG_out_g(X1)) → qcF_out_gg(X1, f(X1))
U88_gg(X1, X2, qcF_out_gg(X1, X2)) → qcF_out_gg(X1, f(X2))
U148_gg(X1, X2, qcF_out_gg(X1, X2)) → rcL_out_gg(X1, X2)
rcL_in_gg(X1, X1) → U149_gg(X1, tcG_in_g(X1))
U149_gg(X1, tcG_out_g(X1)) → rcL_out_gg(X1, X1)
U95_gg(X1, X2, rcL_out_gg(X1, f(X2))) → U96_gg(X1, X2, qcK_in_gg(X1, X2))
U96_gg(X1, X2, qcK_out_gg(X1, X2)) → qcK_out_gg(X1, f(X2))
U97_gg(X1, X2, qcK_out_gg(X1, X2)) → pcM_out_gg(X1, X2)
U150_g(X1, pcM_out_gg(f(f(f(f(f(f(f(f(X1)))))))), X1)) → qcO_out_g(f(f(X1)))
U98_g(X1, qcO_out_g(f(X1))) → U99_g(X1, qcF_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U99_g(X1, qcF_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → rcN_out_g(f(f(X1)))
U100_g(X1, rcN_out_g(f(f(X1)))) → U101_g(X1, qcK_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U101_g(X1, qcK_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → pcP_out_g(f(f(X1)))
U151_g(X1, pcP_out_g(f(X1))) → qcT_out_g(f(f(X1)))
U104_g(X1, qcT_out_g(f(X1))) → U105_g(X1, qcQ_in_g(X1))
U105_g(X1, qcQ_out_g(X1)) → rcS_out_g(f(f(X1)))
U108_g(X1, rcS_out_g(f(f(X1)))) → U109_g(X1, qcU_in_g(X1))
U109_g(X1, qcU_out_g(X1)) → pcW_out_g(f(f(X1)))
U152_g(X1, pcW_out_g(f(X1))) → qcN1_out_g(f(f(X1)))
U112_g(X1, qcN1_out_g(f(X1))) → U113_g(X1, qcX_in_g(X1))
U113_g(X1, qcX_out_g(X1)) → rcZ_out_g(f(f(X1)))
U116_g(X1, rcZ_out_g(f(f(X1)))) → U117_g(X1, qcN2_in_g(X1))
U117_g(X1, qcN2_out_g(X1)) → pcN4_out_g(f(f(X1)))
U153_g(X1, pcN4_out_g(f(X1))) → qcN9_out_g(f(f(X1)))
U122_g(X1, qcN9_out_g(f(X1))) → U123_g(X1, qcN5_in_g(X1))
U123_g(X1, qcN5_out_g(X1)) → rcN8_out_g(f(f(X1)))
U127_g(X1, rcN8_out_g(f(f(X1)))) → U128_g(X1, qcI_in_g(X1))
U128_g(X1, qcI_out_g(X1)) → pcB_out_g(f(f(X1)))
U83_g(X1, pcB_out_g(f(X1))) → qcA_out_g(f(X1))

The set Q consists of the following terms:

qcA_in_g(x0)
pcB_in_g(x0)
rcN8_in_g(x0)
qcN9_in_g(x0)
pcN4_in_g(x0)
rcZ_in_g(x0)
qcN1_in_g(x0)
pcW_in_g(x0)
rcS_in_g(x0)
qcT_in_g(x0)
pcP_in_g(x0)
rcN_in_g(x0)
qcO_in_g(x0)
pcM_in_gg(x0, x1)
qcK_in_gg(x0, x1)
rcL_in_gg(x0, x1)
qcF_in_gg(x0, x1)
qcC_in_gg(x0, x1)
pcD_in_g(x0)
rcN13_in_g(x0)
U140_g(x0, x1)
rcN7_in_g(x0)
qcH_in_g(x0)
qcI_in_g(x0)
rcN10_in_g(x0)
qcN5_in_g(x0)
qcN6_in_g(x0)
qcN2_in_g(x0)
rcN3_in_g(x0)
qcX_in_g(x0)
qcY_in_g(x0)
qcU_in_g(x0)
rcV_in_g(x0)
qcQ_in_g(x0)
qcR_in_g(x0)
U147_g(x0, x1)
U102_g(x0, x1)
U103_g(x0, x1)
U146_g(x0, x1)
U106_g(x0, x1)
U107_g(x0, x1)
U145_g(x0, x1)
U110_g(x0, x1)
U111_g(x0, x1)
U144_g(x0, x1)
U114_g(x0, x1)
U115_g(x0, x1)
U143_g(x0, x1)
U118_g(x0, x1)
U119_g(x0, x1)
U142_g(x0, x1)
U125_g(x0, x1)
U126_g(x0, x1)
U91_g(x0, x1)
U120_g(x0, x1)
tcG_in_g(x0)
qcJ_in_g(x0)
U92_g(x0, x1)
U93_g(x0, x1)
U94_g(x0, x1)
U124_g(x0, x1)
U121_g(x0, x1)
U141_g(x0, x1)
U137_g(x0, x1)
U138_g(x0, x1)
U139_g(x0, x1)
U84_gg(x0, x1)
U85_gg(x0, x1)
qcE_in_gg(x0, x1)
rcN12_in_gg(x0, x1)
qcN11_in_gg(x0, x1)
U129_gg(x0)
U130_gg(x0, x1, x2)
U132_gg(x0, x1)
U133_gg(x0, x1)
U131_gg(x0, x1, x2)
U154_gg(x0, x1, x2)
U155_gg(x0, x1)
U134_gg(x0)
U135_gg(x0, x1, x2)
U136_gg(x0, x1, x2)
U86_gg(x0, x1, x2)
U87_gg(x0, x1, x2)
U89_gg(x0, x1)
U90_gg(x0, x1)
U88_gg(x0, x1, x2)
U148_gg(x0, x1, x2)
U149_gg(x0, x1)
U95_gg(x0, x1, x2)
U96_gg(x0, x1, x2)
U97_gg(x0, x1, x2)
U150_g(x0, x1)
U98_g(x0, x1)
U99_g(x0, x1)
U100_g(x0, x1)
U101_g(x0, x1)
U151_g(x0, x1)
U104_g(x0, x1)
U105_g(x0, x1)
U108_g(x0, x1)
U109_g(x0, x1)
U152_g(x0, x1)
U112_g(x0, x1)
U113_g(x0, x1)
U116_g(x0, x1)
U117_g(x0, x1)
U153_g(x0, x1)
U122_g(x0, x1)
U123_g(x0, x1)
U127_g(x0, x1)
U128_g(x0, x1)
U83_g(x0, x1)

We have to consider all (P,Q,R)-chains.

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


QC_IN_GG(X1, f(f(X1))) → QA_IN_G(X1)
RN8_IN_G(f(f(f(X1)))) → PN4_IN_G(f(X1))
PN4_IN_G(f(X1)) → RZ_IN_G(f(X1))
RZ_IN_G(f(f(f(X1)))) → PW_IN_G(f(X1))
RS_IN_G(f(f(f(X1)))) → PP_IN_G(f(X1))
RN_IN_G(f(f(f(X1)))) → PM_IN_GG(f(f(f(f(f(f(f(f(X1)))))))), X1)
PK_IN_GG(X1, X2) → PF_IN_GG(X1, X2)
QC_IN_GG(X1, f(f(X1))) → U73_GG(X1, qcA_in_g(X1))
QH_IN_G(f(f(X1))) → PI_IN_G(X1)
PI_IN_G(X1) → PN5_IN_G(X1)
PN5_IN_G(f(f(X1))) → PN2_IN_G(X1)
PX_IN_G(f(f(X1))) → PU_IN_G(X1)
PQ_IN_G(f(f(X1))) → PM_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
RN_IN_G(f(f(X1))) → U18_G(X1, qcO_in_g(f(X1)))
PF_IN_GG(X1, f(X2)) → U3_GG(X1, X2, qcC_in_gg(f(X1), f(X2)))
PJ_IN_G(f(X1)) → U9_G(X1, qcH_in_g(f(f(X1))))
PP_IN_G(f(f(X1))) → U21_G(X1, rcN_in_g(f(f(X1))))
PK_IN_GG(X1, f(X2)) → U14_GG(X1, X2, rcL_in_gg(X1, f(X2)))
RS_IN_G(f(f(X1))) → U27_G(X1, qcT_in_g(f(X1)))
PW_IN_G(f(f(X1))) → U33_G(X1, rcS_in_g(f(f(X1))))
RZ_IN_G(f(f(X1))) → U39_G(X1, qcN1_in_g(f(X1)))
U39_G(X1, qcN1_out_g(f(X1))) → PX_IN_G(X1)
PN4_IN_G(f(f(X1))) → U45_G(X1, rcZ_in_g(f(f(X1))))
RN8_IN_G(f(f(X1))) → U54_G(X1, qcN9_in_g(f(X1)))
QC_IN_GG(X1, f(f(X1))) → U75_GG(X1, rcN13_in_g(X1))
PB_IN_G(f(f(X1))) → U61_G(X1, rcN8_in_g(f(f(X1))))
QC_IN_GG(X1, f(f(X1))) → U79_GG(X1, pcD_in_g(X1))
QC_IN_GG(X1, f(f(X2))) → PE_IN_GG(X1, X2)
PE_IN_GG(X1, X2) → PN11_IN_GG(X1, X2)
PN11_IN_GG(X1, f(X2)) → U64_GG(X1, X2, qcC_in_gg(X1, f(X2)))
PE_IN_GG(X1, f(X2)) → U70_GG(X1, X2, rcN12_in_gg(X1, f(X2)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(PB_IN_G(x1)) = x1   
POL(PE_IN_GG(x1, x2)) = 1 + x2   
POL(PF_IN_GG(x1, x2)) = x2   
POL(PI_IN_G(x1)) = 1 + x1   
POL(PJ_IN_G(x1)) = 1 + x1   
POL(PK_IN_GG(x1, x2)) = 1 + x2   
POL(PM_IN_GG(x1, x2)) = 1 + x2   
POL(PN11_IN_GG(x1, x2)) = x2   
POL(PN2_IN_G(x1)) = x1   
POL(PN4_IN_G(x1)) = 1 + x1   
POL(PN5_IN_G(x1)) = x1   
POL(PP_IN_G(x1)) = 1 + x1   
POL(PQ_IN_G(x1)) = 1 + x1   
POL(PU_IN_G(x1)) = 1 + x1   
POL(PW_IN_G(x1)) = x1   
POL(PX_IN_G(x1)) = x1   
POL(QA_IN_G(x1)) = x1   
POL(QC_IN_GG(x1, x2)) = x2   
POL(QH_IN_G(x1)) = x1   
POL(RN7_IN_G(x1)) = x1   
POL(RN8_IN_G(x1)) = x1   
POL(RN_IN_G(x1)) = 1 + x1   
POL(RS_IN_G(x1)) = x1   
POL(RZ_IN_G(x1)) = x1   
POL(TG_IN_G(x1)) = 1 + x1   
POL(U100_g(x1, x2)) = 0   
POL(U101_g(x1, x2)) = 0   
POL(U102_g(x1, x2)) = 0   
POL(U103_g(x1, x2)) = 0   
POL(U104_g(x1, x2)) = 0   
POL(U105_g(x1, x2)) = 0   
POL(U106_g(x1, x2)) = 0   
POL(U107_g(x1, x2)) = 0   
POL(U108_g(x1, x2)) = 0   
POL(U109_g(x1, x2)) = 0   
POL(U110_g(x1, x2)) = 0   
POL(U111_g(x1, x2)) = 0   
POL(U112_g(x1, x2)) = 0   
POL(U113_g(x1, x2)) = 0   
POL(U114_g(x1, x2)) = 0   
POL(U115_g(x1, x2)) = 0   
POL(U116_g(x1, x2)) = 0   
POL(U117_g(x1, x2)) = 0   
POL(U118_g(x1, x2)) = 0   
POL(U119_g(x1, x2)) = 0   
POL(U120_g(x1, x2)) = 0   
POL(U121_g(x1, x2)) = 0   
POL(U122_g(x1, x2)) = 0   
POL(U123_g(x1, x2)) = 0   
POL(U124_g(x1, x2)) = 0   
POL(U125_g(x1, x2)) = 0   
POL(U126_g(x1, x2)) = 0   
POL(U127_g(x1, x2)) = 0   
POL(U128_g(x1, x2)) = 0   
POL(U129_gg(x1)) = 0   
POL(U130_gg(x1, x2, x3)) = 0   
POL(U131_gg(x1, x2, x3)) = 0   
POL(U132_gg(x1, x2)) = 0   
POL(U133_gg(x1, x2)) = 0   
POL(U134_gg(x1)) = 0   
POL(U135_gg(x1, x2, x3)) = 0   
POL(U136_gg(x1, x2, x3)) = 0   
POL(U137_g(x1, x2)) = 0   
POL(U138_g(x1, x2)) = 0   
POL(U139_g(x1, x2)) = 0   
POL(U140_g(x1, x2)) = 0   
POL(U141_g(x1, x2)) = 0   
POL(U142_g(x1, x2)) = 0   
POL(U143_g(x1, x2)) = 0   
POL(U144_g(x1, x2)) = 0   
POL(U145_g(x1, x2)) = 0   
POL(U146_g(x1, x2)) = 0   
POL(U147_g(x1, x2)) = 0   
POL(U148_gg(x1, x2, x3)) = 0   
POL(U149_gg(x1, x2)) = 0   
POL(U14_GG(x1, x2, x3)) = 1 + x2   
POL(U150_g(x1, x2)) = 0   
POL(U151_g(x1, x2)) = 0   
POL(U152_g(x1, x2)) = 0   
POL(U153_g(x1, x2)) = 0   
POL(U154_gg(x1, x2, x3)) = 0   
POL(U155_gg(x1, x2)) = 0   
POL(U18_G(x1, x2)) = x1   
POL(U21_G(x1, x2)) = 1 + x1   
POL(U24_G(x1, x2)) = 1 + x1   
POL(U27_G(x1, x2)) = 1 + x1   
POL(U30_G(x1, x2)) = 1 + x1   
POL(U33_G(x1, x2)) = 1 + x1   
POL(U36_G(x1, x2)) = x1   
POL(U39_G(x1, x2)) = 1 + x1   
POL(U3_GG(x1, x2, x3)) = x2   
POL(U42_G(x1, x2)) = x1   
POL(U45_G(x1, x2)) = x1   
POL(U48_G(x1, x2)) = x1   
POL(U51_G(x1, x2)) = x1   
POL(U54_G(x1, x2)) = x1   
POL(U58_G(x1, x2)) = 1 + x1   
POL(U5_GG(x1, x2)) = 1 + x1   
POL(U61_G(x1, x2)) = 1 + x1   
POL(U64_GG(x1, x2, x3)) = x2   
POL(U66_GG(x1, x2)) = 1 + x1   
POL(U70_GG(x1, x2, x3)) = 1 + x2   
POL(U73_GG(x1, x2)) = x1   
POL(U75_GG(x1, x2)) = x1   
POL(U77_GG(x1, x2)) = x1   
POL(U79_GG(x1, x2)) = x1   
POL(U83_g(x1, x2)) = 0   
POL(U84_gg(x1, x2)) = 0   
POL(U85_gg(x1, x2)) = 0   
POL(U86_gg(x1, x2, x3)) = 0   
POL(U87_gg(x1, x2, x3)) = 0   
POL(U88_gg(x1, x2, x3)) = 0   
POL(U89_gg(x1, x2)) = 0   
POL(U90_gg(x1, x2)) = 0   
POL(U91_g(x1, x2)) = 0   
POL(U92_g(x1, x2)) = 0   
POL(U93_g(x1, x2)) = 0   
POL(U94_g(x1, x2)) = 0   
POL(U95_gg(x1, x2, x3)) = 0   
POL(U96_gg(x1, x2, x3)) = 0   
POL(U97_gg(x1, x2, x3)) = 0   
POL(U98_g(x1, x2)) = 0   
POL(U99_g(x1, x2)) = 0   
POL(U9_G(x1, x2)) = 1 + x1   
POL(a) = 0   
POL(b) = 0   
POL(f(x1)) = 1 + x1   
POL(pcB_in_g(x1)) = 0   
POL(pcB_out_g(x1)) = 0   
POL(pcD_in_g(x1)) = 0   
POL(pcD_out_g(x1)) = 0   
POL(pcM_in_gg(x1, x2)) = 0   
POL(pcM_out_gg(x1, x2)) = 0   
POL(pcN4_in_g(x1)) = 0   
POL(pcN4_out_g(x1)) = 0   
POL(pcP_in_g(x1)) = 0   
POL(pcP_out_g(x1)) = 0   
POL(pcW_in_g(x1)) = 0   
POL(pcW_out_g(x1)) = 0   
POL(qcA_in_g(x1)) = 0   
POL(qcA_out_g(x1)) = 0   
POL(qcC_in_gg(x1, x2)) = 0   
POL(qcC_out_gg(x1, x2)) = 0   
POL(qcE_in_gg(x1, x2)) = 0   
POL(qcE_out_gg(x1, x2)) = 0   
POL(qcF_in_gg(x1, x2)) = 0   
POL(qcF_out_gg(x1, x2)) = 0   
POL(qcH_in_g(x1)) = 0   
POL(qcH_out_g(x1)) = 0   
POL(qcI_in_g(x1)) = 0   
POL(qcI_out_g(x1)) = 0   
POL(qcJ_in_g(x1)) = 0   
POL(qcJ_out_g(x1)) = 0   
POL(qcK_in_gg(x1, x2)) = 0   
POL(qcK_out_gg(x1, x2)) = 0   
POL(qcN11_in_gg(x1, x2)) = 0   
POL(qcN11_out_gg(x1, x2)) = 0   
POL(qcN1_in_g(x1)) = 0   
POL(qcN1_out_g(x1)) = 0   
POL(qcN2_in_g(x1)) = 0   
POL(qcN2_out_g(x1)) = 0   
POL(qcN5_in_g(x1)) = 0   
POL(qcN5_out_g(x1)) = 0   
POL(qcN6_in_g(x1)) = 0   
POL(qcN6_out_g(x1)) = 0   
POL(qcN9_in_g(x1)) = 0   
POL(qcN9_out_g(x1)) = 0   
POL(qcO_in_g(x1)) = 0   
POL(qcO_out_g(x1)) = 0   
POL(qcQ_in_g(x1)) = 0   
POL(qcQ_out_g(x1)) = 0   
POL(qcR_in_g(x1)) = 0   
POL(qcR_out_g(x1)) = 0   
POL(qcT_in_g(x1)) = 0   
POL(qcT_out_g(x1)) = 0   
POL(qcU_in_g(x1)) = 0   
POL(qcU_out_g(x1)) = 0   
POL(qcX_in_g(x1)) = 0   
POL(qcX_out_g(x1)) = 0   
POL(qcY_in_g(x1)) = 0   
POL(qcY_out_g(x1)) = 0   
POL(rcL_in_gg(x1, x2)) = 0   
POL(rcL_out_gg(x1, x2)) = 0   
POL(rcN10_in_g(x1)) = 0   
POL(rcN10_out_g(x1)) = 0   
POL(rcN12_in_gg(x1, x2)) = 0   
POL(rcN12_out_gg(x1, x2)) = 0   
POL(rcN13_in_g(x1)) = 0   
POL(rcN13_out_g(x1)) = 0   
POL(rcN3_in_g(x1)) = 0   
POL(rcN3_out_g(x1)) = 0   
POL(rcN7_in_g(x1)) = 0   
POL(rcN7_out_g(x1)) = 0   
POL(rcN8_in_g(x1)) = 0   
POL(rcN8_out_g(x1)) = 0   
POL(rcN_in_g(x1)) = 0   
POL(rcN_out_g(x1)) = 0   
POL(rcS_in_g(x1)) = 0   
POL(rcS_out_g(x1)) = 0   
POL(rcV_in_g(x1)) = 0   
POL(rcV_out_g(x1)) = 0   
POL(rcZ_in_g(x1)) = 0   
POL(rcZ_out_g(x1)) = 0   
POL(tcG_in_g(x1)) = 0   
POL(tcG_out_g(x1)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QA_IN_G(f(X1)) → PB_IN_G(f(X1))
PB_IN_G(f(X1)) → RN8_IN_G(f(X1))
PW_IN_G(f(X1)) → RS_IN_G(f(X1))
PP_IN_G(f(X1)) → RN_IN_G(f(X1))
PF_IN_GG(X1, X2) → QC_IN_GG(f(X1), X2)
U73_GG(X1, qcA_out_g(X1)) → RN7_IN_G(X1)
RN7_IN_G(X1) → QH_IN_G(X1)
PN2_IN_G(X1) → PX_IN_G(X1)
PU_IN_G(X1) → PQ_IN_G(X1)
PQ_IN_G(X1) → U24_G(X1, qcR_in_g(X1))
U24_G(X1, qcR_out_g(X1)) → RN_IN_G(X1)
U18_G(X1, qcO_out_g(f(X1))) → PF_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
U3_GG(X1, X2, qcC_out_gg(f(X1), f(X2))) → PF_IN_GG(X1, X2)
PF_IN_GG(X1, f(X1)) → U5_GG(X1, qcC_in_gg(f(X1), f(X1)))
U5_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
TG_IN_G(X1) → PJ_IN_G(X1)
PJ_IN_G(X1) → QH_IN_G(f(X1))
U9_G(X1, qcH_out_g(f(f(X1)))) → PJ_IN_G(X1)
PU_IN_G(X1) → U30_G(X1, rcV_in_g(X1))
U30_G(X1, rcV_out_g(X1)) → PP_IN_G(X1)
U21_G(X1, rcN_out_g(f(f(X1)))) → PK_IN_GG(f(f(f(f(f(f(f(X1))))))), X1)
PK_IN_GG(X1, X1) → TG_IN_G(X1)
U14_GG(X1, X2, rcL_out_gg(X1, f(X2))) → PK_IN_GG(X1, X2)
PX_IN_G(X1) → U36_G(X1, qcY_in_g(X1))
U36_G(X1, qcY_out_g(X1)) → RS_IN_G(X1)
U27_G(X1, qcT_out_g(f(X1))) → PQ_IN_G(X1)
PN2_IN_G(X1) → U42_G(X1, rcN3_in_g(X1))
U42_G(X1, rcN3_out_g(X1)) → PW_IN_G(X1)
U33_G(X1, rcS_out_g(f(f(X1)))) → PU_IN_G(X1)
PN5_IN_G(X1) → U48_G(X1, qcN6_in_g(X1))
U48_G(X1, qcN6_out_g(X1)) → RZ_IN_G(X1)
PI_IN_G(X1) → U58_G(X1, rcN10_in_g(X1))
U58_G(X1, rcN10_out_g(X1)) → PN4_IN_G(X1)
U45_G(X1, rcZ_out_g(f(f(X1)))) → PN2_IN_G(X1)
RN7_IN_G(X1) → U51_G(X1, qcH_in_g(X1))
U51_G(X1, qcH_out_g(X1)) → RN8_IN_G(X1)
U54_G(X1, qcN9_out_g(f(X1))) → PN5_IN_G(X1)
RN8_IN_G(f(X1)) → TG_IN_G(X1)
U75_GG(X1, rcN13_out_g(X1)) → RN7_IN_G(X1)
U75_GG(X1, rcN13_out_g(X1)) → U77_GG(X1, rcN7_in_g(X1))
U77_GG(X1, rcN7_out_g(X1)) → PB_IN_G(X1)
U61_G(X1, rcN8_out_g(f(f(X1)))) → PI_IN_G(X1)
U79_GG(X1, pcD_out_g(X1)) → QA_IN_G(X1)
PN11_IN_GG(X1, X2) → QC_IN_GG(X1, X2)
U64_GG(X1, X2, qcC_out_gg(X1, f(X2))) → PN11_IN_GG(X1, X2)
PN11_IN_GG(f(X1), f(X1)) → U66_GG(X1, qcC_in_gg(f(X1), f(X1)))
U66_GG(X1, qcC_out_gg(f(X1), f(X1))) → TG_IN_G(X1)
PE_IN_GG(f(X1), X1) → TG_IN_G(X1)
U70_GG(X1, X2, rcN12_out_gg(X1, f(X2))) → PE_IN_GG(X1, X2)
PM_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0) → PK_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0)
PM_IN_GG(f(f(f(f(f(f(f(z0))))))), z0) → PK_IN_GG(f(f(f(f(f(f(f(z0))))))), z0)

The TRS R consists of the following rules:

qcA_in_g(f(X1)) → U83_g(X1, pcB_in_g(f(X1)))
pcB_in_g(f(f(X1))) → U127_g(X1, rcN8_in_g(f(f(X1))))
rcN8_in_g(f(f(X1))) → U122_g(X1, qcN9_in_g(f(X1)))
qcN9_in_g(f(f(X1))) → U153_g(X1, pcN4_in_g(f(X1)))
pcN4_in_g(f(f(X1))) → U116_g(X1, rcZ_in_g(f(f(X1))))
rcZ_in_g(f(f(X1))) → U112_g(X1, qcN1_in_g(f(X1)))
qcN1_in_g(f(f(X1))) → U152_g(X1, pcW_in_g(f(X1)))
pcW_in_g(f(f(X1))) → U108_g(X1, rcS_in_g(f(f(X1))))
rcS_in_g(f(f(X1))) → U104_g(X1, qcT_in_g(f(X1)))
qcT_in_g(f(f(X1))) → U151_g(X1, pcP_in_g(f(X1)))
pcP_in_g(f(f(X1))) → U100_g(X1, rcN_in_g(f(f(X1))))
rcN_in_g(f(f(X1))) → U98_g(X1, qcO_in_g(f(X1)))
qcO_in_g(f(f(X1))) → U150_g(X1, pcM_in_gg(f(f(f(f(f(f(f(f(X1)))))))), X1))
pcM_in_gg(X1, X2) → U97_gg(X1, X2, qcK_in_gg(X1, X2))
qcK_in_gg(X1, f(X2)) → U95_gg(X1, X2, rcL_in_gg(X1, f(X2)))
rcL_in_gg(X1, X2) → U148_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X2)) → U87_gg(X1, X2, qcC_in_gg(f(X1), f(X2)))
qcC_in_gg(a, b) → qcC_out_gg(a, b)
qcC_in_gg(X1, f(f(X1))) → U84_gg(X1, pcD_in_g(X1))
pcD_in_g(X1) → U137_g(X1, rcN13_in_g(X1))
rcN13_in_g(X1) → U140_g(X1, qcA_in_g(X1))
U140_g(X1, qcA_out_g(X1)) → U141_g(X1, rcN7_in_g(X1))
rcN7_in_g(X1) → U120_g(X1, qcH_in_g(X1))
qcH_in_g(f(f(X1))) → U91_g(X1, qcI_in_g(X1))
qcI_in_g(X1) → U125_g(X1, rcN10_in_g(X1))
rcN10_in_g(X1) → U142_g(X1, qcN5_in_g(X1))
qcN5_in_g(X1) → U118_g(X1, qcN6_in_g(X1))
qcN6_in_g(f(f(X1))) → U143_g(X1, qcN2_in_g(X1))
qcN2_in_g(X1) → U114_g(X1, rcN3_in_g(X1))
rcN3_in_g(X1) → U144_g(X1, qcX_in_g(X1))
qcX_in_g(X1) → U110_g(X1, qcY_in_g(X1))
qcY_in_g(f(f(X1))) → U145_g(X1, qcU_in_g(X1))
qcU_in_g(X1) → U106_g(X1, rcV_in_g(X1))
rcV_in_g(X1) → U146_g(X1, qcQ_in_g(X1))
qcQ_in_g(X1) → U102_g(X1, qcR_in_g(X1))
qcR_in_g(f(f(X1))) → U147_g(X1, pcM_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U147_g(X1, pcM_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → qcR_out_g(f(f(X1)))
U102_g(X1, qcR_out_g(X1)) → U103_g(X1, rcN_in_g(X1))
U103_g(X1, rcN_out_g(X1)) → qcQ_out_g(X1)
U146_g(X1, qcQ_out_g(X1)) → rcV_out_g(X1)
U106_g(X1, rcV_out_g(X1)) → U107_g(X1, pcP_in_g(X1))
U107_g(X1, pcP_out_g(X1)) → qcU_out_g(X1)
U145_g(X1, qcU_out_g(X1)) → qcY_out_g(f(f(X1)))
U110_g(X1, qcY_out_g(X1)) → U111_g(X1, rcS_in_g(X1))
U111_g(X1, rcS_out_g(X1)) → qcX_out_g(X1)
U144_g(X1, qcX_out_g(X1)) → rcN3_out_g(X1)
U114_g(X1, rcN3_out_g(X1)) → U115_g(X1, pcW_in_g(X1))
U115_g(X1, pcW_out_g(X1)) → qcN2_out_g(X1)
U143_g(X1, qcN2_out_g(X1)) → qcN6_out_g(f(f(X1)))
U118_g(X1, qcN6_out_g(X1)) → U119_g(X1, rcZ_in_g(X1))
U119_g(X1, rcZ_out_g(X1)) → qcN5_out_g(X1)
U142_g(X1, qcN5_out_g(X1)) → rcN10_out_g(X1)
U125_g(X1, rcN10_out_g(X1)) → U126_g(X1, pcN4_in_g(X1))
U126_g(X1, pcN4_out_g(X1)) → qcI_out_g(X1)
U91_g(X1, qcI_out_g(X1)) → qcH_out_g(f(f(X1)))
U120_g(X1, qcH_out_g(X1)) → U121_g(X1, rcN8_in_g(X1))
rcN8_in_g(f(X1)) → U124_g(X1, tcG_in_g(X1))
tcG_in_g(X1) → U94_g(X1, qcJ_in_g(X1))
qcJ_in_g(f(X1)) → U92_g(X1, qcH_in_g(f(f(X1))))
U92_g(X1, qcH_out_g(f(f(X1)))) → U93_g(X1, qcJ_in_g(X1))
U93_g(X1, qcJ_out_g(X1)) → qcJ_out_g(f(X1))
U94_g(X1, qcJ_out_g(X1)) → tcG_out_g(X1)
U124_g(X1, tcG_out_g(X1)) → rcN8_out_g(f(X1))
U121_g(X1, rcN8_out_g(X1)) → rcN7_out_g(X1)
U141_g(X1, rcN7_out_g(X1)) → rcN13_out_g(X1)
U137_g(X1, rcN13_out_g(X1)) → U138_g(X1, rcN7_in_g(X1))
U138_g(X1, rcN7_out_g(X1)) → U139_g(X1, pcB_in_g(X1))
U139_g(X1, pcB_out_g(X1)) → pcD_out_g(X1)
U84_gg(X1, pcD_out_g(X1)) → U85_gg(X1, qcA_in_g(X1))
U85_gg(X1, qcA_out_g(X1)) → qcC_out_gg(X1, f(f(X1)))
qcC_in_gg(X1, f(f(X2))) → U86_gg(X1, X2, qcE_in_gg(X1, X2))
qcE_in_gg(a, b) → U134_gg(rcN12_in_gg(a, b))
rcN12_in_gg(X1, X2) → U154_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(a, b) → U129_gg(qcC_in_gg(a, b))
U129_gg(qcC_out_gg(a, b)) → qcN11_out_gg(a, b)
qcN11_in_gg(X1, f(X2)) → U130_gg(X1, X2, qcC_in_gg(X1, f(X2)))
U130_gg(X1, X2, qcC_out_gg(X1, f(X2))) → U131_gg(X1, X2, qcN11_in_gg(X1, X2))
qcN11_in_gg(f(X1), f(X1)) → U132_gg(X1, qcC_in_gg(f(X1), f(X1)))
U132_gg(X1, qcC_out_gg(f(X1), f(X1))) → U133_gg(X1, tcG_in_g(X1))
U133_gg(X1, tcG_out_g(X1)) → qcN11_out_gg(f(X1), f(X1))
U131_gg(X1, X2, qcN11_out_gg(X1, X2)) → qcN11_out_gg(X1, f(X2))
U154_gg(X1, X2, qcN11_out_gg(X1, X2)) → rcN12_out_gg(X1, X2)
rcN12_in_gg(f(X1), X1) → U155_gg(X1, tcG_in_g(X1))
U155_gg(X1, tcG_out_g(X1)) → rcN12_out_gg(f(X1), X1)
U134_gg(rcN12_out_gg(a, b)) → qcE_out_gg(a, b)
qcE_in_gg(X1, f(X2)) → U135_gg(X1, X2, rcN12_in_gg(X1, f(X2)))
U135_gg(X1, X2, rcN12_out_gg(X1, f(X2))) → U136_gg(X1, X2, qcE_in_gg(X1, X2))
U136_gg(X1, X2, qcE_out_gg(X1, X2)) → qcE_out_gg(X1, f(X2))
U86_gg(X1, X2, qcE_out_gg(X1, X2)) → qcC_out_gg(X1, f(f(X2)))
U87_gg(X1, X2, qcC_out_gg(f(X1), f(X2))) → U88_gg(X1, X2, qcF_in_gg(X1, X2))
qcF_in_gg(X1, f(X1)) → U89_gg(X1, qcC_in_gg(f(X1), f(X1)))
U89_gg(X1, qcC_out_gg(f(X1), f(X1))) → U90_gg(X1, tcG_in_g(X1))
U90_gg(X1, tcG_out_g(X1)) → qcF_out_gg(X1, f(X1))
U88_gg(X1, X2, qcF_out_gg(X1, X2)) → qcF_out_gg(X1, f(X2))
U148_gg(X1, X2, qcF_out_gg(X1, X2)) → rcL_out_gg(X1, X2)
rcL_in_gg(X1, X1) → U149_gg(X1, tcG_in_g(X1))
U149_gg(X1, tcG_out_g(X1)) → rcL_out_gg(X1, X1)
U95_gg(X1, X2, rcL_out_gg(X1, f(X2))) → U96_gg(X1, X2, qcK_in_gg(X1, X2))
U96_gg(X1, X2, qcK_out_gg(X1, X2)) → qcK_out_gg(X1, f(X2))
U97_gg(X1, X2, qcK_out_gg(X1, X2)) → pcM_out_gg(X1, X2)
U150_g(X1, pcM_out_gg(f(f(f(f(f(f(f(f(X1)))))))), X1)) → qcO_out_g(f(f(X1)))
U98_g(X1, qcO_out_g(f(X1))) → U99_g(X1, qcF_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U99_g(X1, qcF_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → rcN_out_g(f(f(X1)))
U100_g(X1, rcN_out_g(f(f(X1)))) → U101_g(X1, qcK_in_gg(f(f(f(f(f(f(f(X1))))))), X1))
U101_g(X1, qcK_out_gg(f(f(f(f(f(f(f(X1))))))), X1)) → pcP_out_g(f(f(X1)))
U151_g(X1, pcP_out_g(f(X1))) → qcT_out_g(f(f(X1)))
U104_g(X1, qcT_out_g(f(X1))) → U105_g(X1, qcQ_in_g(X1))
U105_g(X1, qcQ_out_g(X1)) → rcS_out_g(f(f(X1)))
U108_g(X1, rcS_out_g(f(f(X1)))) → U109_g(X1, qcU_in_g(X1))
U109_g(X1, qcU_out_g(X1)) → pcW_out_g(f(f(X1)))
U152_g(X1, pcW_out_g(f(X1))) → qcN1_out_g(f(f(X1)))
U112_g(X1, qcN1_out_g(f(X1))) → U113_g(X1, qcX_in_g(X1))
U113_g(X1, qcX_out_g(X1)) → rcZ_out_g(f(f(X1)))
U116_g(X1, rcZ_out_g(f(f(X1)))) → U117_g(X1, qcN2_in_g(X1))
U117_g(X1, qcN2_out_g(X1)) → pcN4_out_g(f(f(X1)))
U153_g(X1, pcN4_out_g(f(X1))) → qcN9_out_g(f(f(X1)))
U122_g(X1, qcN9_out_g(f(X1))) → U123_g(X1, qcN5_in_g(X1))
U123_g(X1, qcN5_out_g(X1)) → rcN8_out_g(f(f(X1)))
U127_g(X1, rcN8_out_g(f(f(X1)))) → U128_g(X1, qcI_in_g(X1))
U128_g(X1, qcI_out_g(X1)) → pcB_out_g(f(f(X1)))
U83_g(X1, pcB_out_g(f(X1))) → qcA_out_g(f(X1))

The set Q consists of the following terms:

qcA_in_g(x0)
pcB_in_g(x0)
rcN8_in_g(x0)
qcN9_in_g(x0)
pcN4_in_g(x0)
rcZ_in_g(x0)
qcN1_in_g(x0)
pcW_in_g(x0)
rcS_in_g(x0)
qcT_in_g(x0)
pcP_in_g(x0)
rcN_in_g(x0)
qcO_in_g(x0)
pcM_in_gg(x0, x1)
qcK_in_gg(x0, x1)
rcL_in_gg(x0, x1)
qcF_in_gg(x0, x1)
qcC_in_gg(x0, x1)
pcD_in_g(x0)
rcN13_in_g(x0)
U140_g(x0, x1)
rcN7_in_g(x0)
qcH_in_g(x0)
qcI_in_g(x0)
rcN10_in_g(x0)
qcN5_in_g(x0)
qcN6_in_g(x0)
qcN2_in_g(x0)
rcN3_in_g(x0)
qcX_in_g(x0)
qcY_in_g(x0)
qcU_in_g(x0)
rcV_in_g(x0)
qcQ_in_g(x0)
qcR_in_g(x0)
U147_g(x0, x1)
U102_g(x0, x1)
U103_g(x0, x1)
U146_g(x0, x1)
U106_g(x0, x1)
U107_g(x0, x1)
U145_g(x0, x1)
U110_g(x0, x1)
U111_g(x0, x1)
U144_g(x0, x1)
U114_g(x0, x1)
U115_g(x0, x1)
U143_g(x0, x1)
U118_g(x0, x1)
U119_g(x0, x1)
U142_g(x0, x1)
U125_g(x0, x1)
U126_g(x0, x1)
U91_g(x0, x1)
U120_g(x0, x1)
tcG_in_g(x0)
qcJ_in_g(x0)
U92_g(x0, x1)
U93_g(x0, x1)
U94_g(x0, x1)
U124_g(x0, x1)
U121_g(x0, x1)
U141_g(x0, x1)
U137_g(x0, x1)
U138_g(x0, x1)
U139_g(x0, x1)
U84_gg(x0, x1)
U85_gg(x0, x1)
qcE_in_gg(x0, x1)
rcN12_in_gg(x0, x1)
qcN11_in_gg(x0, x1)
U129_gg(x0)
U130_gg(x0, x1, x2)
U132_gg(x0, x1)
U133_gg(x0, x1)
U131_gg(x0, x1, x2)
U154_gg(x0, x1, x2)
U155_gg(x0, x1)
U134_gg(x0)
U135_gg(x0, x1, x2)
U136_gg(x0, x1, x2)
U86_gg(x0, x1, x2)
U87_gg(x0, x1, x2)
U89_gg(x0, x1)
U90_gg(x0, x1)
U88_gg(x0, x1, x2)
U148_gg(x0, x1, x2)
U149_gg(x0, x1)
U95_gg(x0, x1, x2)
U96_gg(x0, x1, x2)
U97_gg(x0, x1, x2)
U150_g(x0, x1)
U98_g(x0, x1)
U99_g(x0, x1)
U100_g(x0, x1)
U101_g(x0, x1)
U151_g(x0, x1)
U104_g(x0, x1)
U105_g(x0, x1)
U108_g(x0, x1)
U109_g(x0, x1)
U152_g(x0, x1)
U112_g(x0, x1)
U113_g(x0, x1)
U116_g(x0, x1)
U117_g(x0, x1)
U153_g(x0, x1)
U122_g(x0, x1)
U123_g(x0, x1)
U127_g(x0, x1)
U128_g(x0, x1)
U83_g(x0, x1)

We have to consider all (P,Q,R)-chains.

(13) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 51 less nodes.

(14) TRUE